A Production-Ready RL Recipe for Formal Proofs
Project Numina just dropped Kimina-Prover-RL, an open-source reinforcement learning pipeline for training language models to write formal proofs in Lean 4. This isn't a research demo—it's a complete training recipe built on top of the Verl RL framework, packaged with everything you need to reproduce their results or adapt it to your own theorem-proving work.
The release includes two new models that set state-of-the-art benchmarks for their size classes: a 1.7B parameter model hitting 76.63% Pass@32 on MiniF2F, and a 0.6B model reaching 71.30%. Both are genuinely small models punching above their weight in formal mathematics.
What makes this interesting isn't just the numbers—it's that the entire pipeline is out there for anyone to use, complete with the specific GRPO configuration, dataset filtering strategy, and infrastructure for high-throughput Lean verification.
The DeepSeek-R1 Connection: Reasoning Then Code
The core design borrows heavily from DeepSeek-R1's structured output approach: models first emit a natural-language reasoning trace inside <think> tags, then follow it with actual Lean 4 proof code. This separation of planning from execution isn't just about interpretability—it gives the model room to reason through proof strategies before committing to formal tactics.
During training, the model learns to structure every response as:
- A
<think>...</think>block explaining the proof strategy - A Lean 4 code block with the actual formal proof
The pipeline enforces this structure hard. Any rollout that doesn't conform—missing the thinking block, wrong ordering, malformed code—gets zero reward, even if the underlying proof would've been valid. This strictness teaches the model to be reliably structured, not just occasionally correct.
Format Rewards: Beyond Simple Validation
The format checking goes deeper than just verifying block presence. While the open-source release includes core format validation, the full Kimina-Prover system (which this pipeline is simplified from) layers on additional checks:
- Rejecting outputs with repetitive reasoning lines that signal degenerate generation
- Requiring a minimum number of tactic blocks in the reasoning section
- Checking comment density thresholds to penalize verbose boilerplate
- Measuring semantic alignment between tactics described in reasoning and the final Lean code
- Penalizing unnecessarily long responses to encourage token efficiency
Only generations passing these checks are eligible for rewards. It's a thoughtful approach to combating the kind of shortcut solutions that plague RL training—models that game the reward signal by outputting garbage that accidentally passes simple validation.
Error Correction: Learning From Lean Feedback
Here's where it gets clever: when a rollout fails (Lean compilation error, incorrect proof, whatever), the pipeline doesn't just discard it. Instead, it creates a new training sample where the model is explicitly prompted to revise its previous attempt, with the Lean error message included in the prompt.
This multi-turn interaction lets the model learn from failure signals directly. Instead of only being rewarded for first-attempt success, it gets credit for debugging its own proofs. The pipeline caps this at one error-fix turn to keep response lengths manageable, and truncates error messages to a fixed token budget.
The results show this matters: after training, the 1.7B model jumps from 76.23% Pass@32 to 77.87% when allowed one error-correction turn.
GRPO and the Length Bias Problem
The pipeline uses GRPO (Group Relative Policy Optimization) for training, but switches to a variant called DrGRPO to address a specific pathology. Recent work has shown that standard GRPO exhibits optimization bias toward longer responses, especially for incorrect outputs—the model learns to pad failures with extra tokens.
DrGRPO normalizes token-level losses with a global constant to eliminate this length bias. During training, the team observed average output length increasing (expected under DeepSeek-R1-style reasoning training), but in a controlled way that correlates with better reasoning, not gaming.
Infrastructure: High-Throughput Lean Verification
Training theorem provers at scale requires verifying thousands of proof candidates in parallel. Numina and Kimi built kimina-lean-server specifically for this: an open-source server supporting parallel Lean 4 proof checking at the throughput RL training demands.
They paired it with kimina-client, a lightweight Python package on PyPI that provides a clean API for batching verification requests. This is the kind of unglamorous infrastructure work that makes research reproducible—you can't just hand-wave "verify proofs efficiently" when you're generating 2,048 rollouts per training step.
Dataset: Filtering for Challenge
The training data comes from Kimina-Prover-Promptset, a filtered subset of NuminaMath-LEAN. The filtering strategy is straightforward but opinionated:
- Remove easy problems (historical win rate above 0.5) to focus on challenging statements
- Generate problem variants using Gemini to increase diversity
- Duplicate hard problems to weight them more heavily during training
This bias toward difficulty makes sense for RL—you want training samples at the edge of the model's capabilities, not problems it already solves reliably.
Training Configuration and Results
The provided config targets an 8-GPU setup. Each training step samples 256 problems (half of which are error-correction samples), generates 8 rollouts per sample (2,048 total generations), and evaluates every 5 steps using best@8.
After 48 hours on 8 H100s, the pipeline improved the base AI-MO/Kimina-Prover-Distill-1.7B model by 4 percentage points, reaching 70% on best@8 and 74% after error correction. Format errors steadily decreased over training—a sign the model was internalizing the structured output requirement, not just occasionally getting lucky.
Final Pass@32 numbers show consistent improvement:
- 1.7B model: 72.95% → 76.23% (77.87% with error fixing)
- 0.6B model: 68.85% → 71.30%
These are meaningful gains for models in this size range, especially on MiniF2F, which has become a standard benchmark for formal math reasoning.
Why This Matters
Open-source RL for formal theorem proving has been more talk than walk. Plenty of papers describe training procedures in the abstract; far fewer release the actual training code, let alone a complete recipe you can run.
Kimina-Prover-RL ships as a fork of Verl with everything in recipe/kimina-prover-rl: configs, dataset preprocessing, reward logic, evaluation scripts. If you want to reproduce their results or adapt this to a different base model or proof assistant, you have a real starting point.
The structured reasoning approach also generalizes beyond theorem proving. The same recipe—enforce output structure through format rewards, inject error feedback for multi-turn correction, use length-normalized optimization—could apply to any domain where you need reliable structured outputs and have access to a verifier.
Formal mathematics is a perfect testbed because Lean is the verifier. You get unambiguous binary feedback on every generation. But the patterns here—separating reasoning from execution, learning from compiler errors, fighting length bias in RL—those show up everywhere.
What's Missing
The open-source release is explicitly a "slimmed-down" version of the full Kimina-Prover training system. Some of the more sophisticated format checks (semantic alignment between reasoning and code, tactic coverage metrics) are described but not fully implemented in the public version.
That's fine—releasing 80% of a production system is better than releasing nothing. But it does mean there's likely still a gap between what you can achieve with the public recipe and what the team achieved with their internal pipeline.
The other question is how this scales. The provided config is for 8 GPUs and suggests increasing rollout count if you have multiple nodes, but there's no guidance on how the approach performs at larger scale or with bigger base models. The 1.7B and 0.6B results are impressive for small models, but it's unclear whether the same recipe would yield similar relative improvements on, say, a 70B base.
The Bigger Picture
Formal theorem proving is having a moment. Between Lean 4's growing mathlib, increasing interest in AI for mathematics (see IMO grand challenges, Minimo, all of Project Numina's work), and renewed attention to verifiable reasoning post-o1, we're seeing real infrastructure investment in this space.
Kimina-Prover-RL is part of that build-out. It's not flashy—it's a training pipeline—but it's the kind of tooling that lets more people actually work in this area rather than just read papers about it.
If you're interested in formal methods, RL for reasoning, or just want to see what production training infrastructure looks like when it's done right, the recipe README is worth reading. This is how you ship research.