A tiny 0.6B model just crushed formal math proofs, topping the MiniF2F leaderboard

A new open-source training recipe is producing absurdly strong theorem-proving models that fit on a laptop. The team behind the Kimina Prover has released kimina-prover-rl, a pipeline that teaches small language models to tackle formal mathematics in Lean 4 with a structure borrowed straight from DeepSeek-R1’s playbook: think first, then write code.

The results are genuinely startling for the model sizes involved. Their 1.7-billion-parameter model hits 76.63% Pass@32 on the MiniF2F benchmark, a notoriously tough test for formal proof systems. Even more impressively, a 0.6B-parameter variant achieves 71.30%. Both numbers represent a new state of the art for open-source models in their respective size categories. You can run these things on hardware that wouldn’t break a sweat playing a YouTube video.

The secret sauce isn’t just the model architecture. It’s the training pipeline, now fully open-sourced as a fork of the Verl reinforcement learning framework. The system uses Group Relative Policy Optimization (GRPO), where the model generates multiple proof attempts for each problem. A custom verification server, kimina-lean-server, checks the generated Lean 4 code at scale. The model gets a reward of 1 only if the code compiles and the proof is verified. No partial credit.

Two clever training tricks stand out. First, a strict format reward forces the model to separate its natural language reasoning inside tags from the formal code block. If the structure is wrong—a missing tag, repetitive loops, too many comment lines—the reward is a flat zero, even if the proof was mathematically correct. Second, an error correction turn lets the model see failure signals and try again, baking in a kind of self-repair mechanism. The training data itself, a curated subset of NuminaMath-LEAN, was aggressively filtered to remove easy problems and enriched with synthetic variants from Gemini to boost diversity on hard theorems. The pipeline is fully documented, with all recipes available, so anyone can reproduce the results or adapt them to their own models.