Opening article
Kimina-Prover-RL is an open-source training pipeline for formal theorem proving in Lean 4, inspired by DeepSeek-R1. Released as a fork of Verl, the pipeline combines structured reasoning, GRPO optimization, and error correction to improve open-source models.
A slimmed-down training pipeline from Kimina Prover, with core features and full compatibility with verl.
We are happy to introduce kimina-prover-rl, an open-source training pipeline for formal theorem proving in Lean 4, based on a structured reasoning-then-generation paradigm inspired by DeepSeek-R1.
This training pipelinee is a simplified version of the system we used to train Kimina Prover , preserving the key components of the system and offering full compatibility with the open-source Verl framework.
To train models under this reasoning framework, we apply GRPO — a reinforcement learning approach tailored for LLMs. This open-source version of the training pipeline of Kimina-prover is implemented using the RL library Verl .
With Kimina-Prover-RL , we provide a lightweight yet powerful reinforcement learning pipeline for training Lean 4 theorem provers.
By combining structured reasoning, format rewards, and error correction, we achieve state-of-the-art results for open-source models in the 0.6B–1.7B parameter range.
Each rollout is verified to ensure that this format is respected. If the output is malformed — e.g., missing the <think> block or misplacing the code — the model receives a zero reward , regardless of whether the proof is actually valid.
In parallel, we observe that the number of format errors steadily decreases over the course of training, indicating that the model is learning to produce structurally valid outputs.
It is released as part of a fork of Verl containing the complete training recipe in recipe/kimina-prover-rl , allowing anyone to reproduce our experiments or adapt the setup to their own models and datasets. All information to setup and launch the pipeline can be found in the README of the recipe.
kimina-prover-rl is a training pipeline designed to teach large language models to solve formal proof goals in Lean 4, using a two-stage output structure: a natural language reasoning trace followed by corresponding Lean code.
This paradigm, inspired by DeepSeek-R1, enables the model to separate planning from execution, promoting explainability, error recovery, and stronger generalization.
This release provides the open-source community with a complete reinforcement learning recipe and high-throughput tools for formal mathematical reasoning in Lean 4. It demonstrates scalable performance improvements for smaller parameter models.