Kimina-Prover: reaching 92.2% on miniF2F with whole-proof RL and no search tree

The problem it solves: moving proof search out of symbolic systems and into a language model

Automated theorem proving has two old routes. One is symbolic search (clause-level or tactic-level tree search): reliable, but the heuristics must be rewritten for each new class of statement. The other is an end-to-end neural model: it generalises better, but on Lean 4 it sat stuck between 50% and 70% for a long time because the training signal is so sparse - a competition problem either checks as a whole or fails entirely, with no gradient in between. Kimina-Prover takes a third route: run large-scale reinforcement learning directly on whole-proof generation, with no intermediate prover feedback at all, letting the model write an informal reasoning sketch first and then land it as Lean code.

The bet is that with a big enough model, a long enough context and enough RL scale, search can be internalised into a single generation instead of being bolted on as a tree. The Preview technical report (arXiv:2504.11354) states this position explicitly - they deliberately do not use Monte Carlo tree search, value functions or process reward models (PRM), consistent with the Kimi k1.5 findings. That was contrarian at the time: the AlphaProof line was buying quality precisely with massive search.

Two generations of readings: 80.7% for Preview, 92.2% for 72B

Kimina has two public readings less than three months apart. They must be kept separate, otherwise the two numbers collapse into one.

• Kimina-Prover Preview (2025-04): 80.7% on miniF2F-test (pass@8192), the first published result above 80%, ahead of the previous SOTA BFS-Prover (72.9%) and well ahead of Hunyuan-Prover, DeepSeek-Prover and Leanabelle-Prover. It also holds at small budgets - 68.85% at pass@32 and 65.16% at pass@8 - which is more convincing than the pass@8192 headline alone.
• Kimina-Prover-72B (2025-07-10): with TTRL search and error fixing added, miniF2F reaches 92.2%, the highest public reading on that benchmark as catalogued here.

The 72B post includes a table at equivalent sampling budgets. Same-axis comparisons are rare in this domain, so it is worth reading row by row:

Model	pass@1	pass@32	pass@1024
Kimina-Prover-1.7B	46.7	73.4	-
DSP+	52.5	71.3	80.7
DeepSeek-Prover-V2-7B	58.6	75.6	79.9
Kimina-Prover-8B	61.1	78.3	-
DeepSeek-Prover-V2-671B	61.9	82.4	86.6
Kimina-Prover-72B	63.9	84.0	87.7

Three things follow. First, 72B beat 671B: at under a tenth of the parameters it leads on all three budgets, which is direct evidence that the RL recipe is worth more than base-model scale. Second, pass@1 to pass@1024 gains 23.8 points (63.9 to 87.7), meaning a large share of this model's capability has to be bought with sampling; the honest single-call level is 63.9%. Third, the 8B distillation (61.1) is already level with the 671B DeepSeek-Prover-V2 (61.9), so the small-model deployment path works.

One caveat on the table: it was published by the Kimina team, and the DeepSeek rows are their re-runs rather than DeepSeek's own numbers. DeepSeek reports 88.9% on MiniF2F-test at a larger sampling budget; the two figures do not contradict, they simply use different axes. We therefore catalogue both assets side by side without ranking them.

Four design choices

Choice	What it means	Cost and payoff
Whole-proof generation, no prover feedback	No intermediate feedback during training or testing; the complete proof is emitted in one pass	Simple to engineer and end-to-end trainable with RL; the cost is sample efficiency, patched by larger budgets
Model-size scaling	Base is Qwen2.5-72B, demonstrating that neural theorem provers do show scale effects	The curve had not been clearly observed in the field before; one of Preview's main scientific contributions
Long context	Up to 32K tokens for RL training and inference	The longest in the neural theorem proving community at the time; long proofs and mathlib lemma signatures fit
Formal Reasoning Pattern	A custom reasoning format bridging formal verification and informal mathematical intuition	Informal sketch first, Lean second - the design that made RL converge

The Formal Reasoning Pattern is the easiest piece to underestimate and the most consequential. Pure Lean output is close to unlearnable under RL: the action space is tactic syntax and the reward is sparse and binary. Having the model produce a structured natural-language derivation before translating it into formal code restates a sparse-reward problem as a problem language models are already good at. That is also why they could drop the PRM - the reasoning sketch carries part of the process supervision itself.

What the 72B generation added

Between Preview and 72B the ceiling of single-pass whole-proof generation showed: hard problems needing long, multi-stage lemma chains cannot be produced in one shot. The two additions target exactly that.

• TTRL search (test-time reinforcement learning) plus a lemma-enabled pattern: a trainable agentic proving framework in which the model recursively discovers, combines and reuses intermediate lemmas at test time. It is not a bolted-on symbolic searcher - "split into lemmas" becomes an action the model learns. The 84.0% pass@32 reading comes from this framework.
• Error fixing: the model reads Lean's error messages and proposes targeted corrections. The published progression is pass@32 84.0% - one round of error correction 86.4% - pass@1024 87.7% - full TTRL search 92.2%. The point is that repairing a broken proof is far cheaper than regenerating from scratch, so what improves is sample efficiency, not just a headline number.

Note that both additions run opposite to Preview's stated position: Preview insisted on no prover feedback, and 72B reads prover errors; Preview insisted on no search, and 72B adds test-time search. That is not a contradiction but a typical route evolution - push the baseline to 80% with the simplest possible recipe, then add the omitted machinery back on demand. We keep both generations inside one asset precisely so that evolution stays visible.

The open-source surface: the parts with more reuse value than the model

• Distilled models: Kimina-Prover-Distill-8B (on Qwen3-8B) and 1.7B (on Qwen3-1.7B); the Preview generation shipped 7B and 1.5B. The 8B distillation reaches 61.1% pass@1 on miniF2F, a single-GPU level.
• An autoformalisation model: natural-language statement to Lean statement. It is the only stage in the pipeline without a pass-rate halo, and the one that fails first in real use, so releasing it separately matters.
• Kimina Lean Server (project-numina/kimina-lean-server, about 211 stars): the Lean server and client SDK used throughout their own training. Teams doing formal RL are usually short of exactly this - a Lean service that survives high-concurrency checking - and it has the highest engineering reuse value here.
• A rectified miniF2F-test: they found at least five problems in the original benchmark that were wrongly formalised and published a corrected version. This is a concrete case of a model becoming strong enough to audit its own benchmark; readings on the original and the rectified set are not directly comparable.
• Proof text: every proof Preview found on miniF2F-test is released as a ZIP (compressed to avoid training-data contamination).

Boundaries

• 92.2% is a post-search reading, not a single call: pass@1 is 63.9%. Production cost must be computed over sampling plus search plus error-fixing rounds, not over one API call.
• miniF2F is close to saturated: a 244-problem high-school/competition set pushed past 92% is losing its power to separate frontier models. The next yardstick for this domain should be PutnamBench or Erdős-style problems, and this site has not integrated either.
• The repository declares no open-source licence: GitHub's license field is empty in practice. The technical report, README and proof ZIP are readable, but the legal reuse boundary for code and weights is unclear - confirm the per-model terms on Hugging Face before any commercial use.
• The comparison table is a self-run: the DeepSeek and DSP+ rows were executed by the Kimina team, and protocol details (sampling temperature, mathlib version, Lean version) are not published item by item, so strictly this is a vendor-grade horizontal comparison.
• Lean 4 only: Isabelle and Coq are outside the capability surface, and the error rate of autoformalisation is inside none of the pass-rate numbers.

Our verification status

Facts come from three sources read in full: the MoonshotAI/Kimina-Prover-Preview GitHub README (376 stars / 32 forks, default branch master, last pushed 2025-07-10), the Hugging Face post "Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models" (2025-07-10, source of every row in the table above), and the technical report arXiv:2504.11354. The repository, proof ZIP and distilled models are public, so anyone can verify the proof text independently in Lean 4.

Confidence is graded C (vendor claim), for exactly the same reason as DeepSeek-Prover-V2: we have not run these proofs. We did not recompute 92.2% on a pinned Lean 4 and mathlib version, did not re-run the DeepSeek rows in that table, and did not put both labs back on one axis using the rectified miniF2F-test. Reaching grade A would require pinning Lean 4 and mathlib commits, feeding the proof ZIP to the checker one entry at a time to count real acceptance, re-running Kimina and DeepSeek-Prover-V2 at equal sampling budgets, and reporting both the pass@1 and pass@8192 readings.

One more thing readers should know that we cannot fix: this domain has no third-party board. None of the twelve third-party leaderboards this site syncs covers formal mathematics, so every reading here is lab-reported and horizontal comparisons should be read as direction, not level.