AI-MO Releases Kimina-Prover-RL, Open-Source Pipeline for Lean 4 Theorem Proving

AI-MO has unveiled Kimina-Prover-RL, an open-source training pipeline for teaching large language models to solve formal proof goals in Lean 4. The system separates reasoning from execution—inspired by DeepSeek-R1—and uses reinforcement learning to improve model performance on structured mathematical proofs.

Two New Models Released#

The pipeline produced two state-of-the-art models in their size categories:

• Kimina-Prover-RL-1.7B: Achieves 76.63% Pass@32 on the MiniF2F benchmark
• Kimina-Prover-RL-0.6B: Achieves 71.30% Pass@32 on the MiniF2F benchmark

Both significantly outperform prior open-source baselines of similar scale.

How the Pipeline Works#

The training uses a two-stage output structure:

1. A reasoning block (<think>) where the model plans its approach
2. A Lean 4 code block containing the formal proof

During training, the model generates multiple candidate proofs per problem. Rewards are assigned only to outputs whose Lean code passes formal verification—verified by an open-source server called kimina-lean-server, developed by Numina and Kimi to handle parallel proof checking at scale.

Key Training Features#

Format Checking Reward: The model learns to structure outputs consistently, with checks for proper think/code block separation, reasonable comment density, and semantic alignment between reasoning and code.

Error Correction Mechanism: When a proof fails, the model receives the Lean error feedback and is given a chance to revise and fix its own work—teaching it to learn from failure signals across multiple turns.

Optimized for Length Bias: The team adopted DrGPO (a variant of GRPO) to normalize token-level losses and eliminate artificial length inflation, addressing optimization bias observed in similar training approaches.

Dataset & Training Setup#

Models were trained on , a filtered subset of NuminaMath-LEAN featuring: