DeepSeek-Prover-V2: making the Lean kernel, not the model, the judge of correctness
deepseek-prover-v2
DeepSeek's formal theorem proving model: a 671B MoE base shared with DeepSeek-V3 and Lean 4 as target language, so formal alignment on a flagship base. The core move is recursive subgoal decomposition at cold start: one-shot proofs of competition statements succeed so rarely that RL has almost no positive samples, so DeepSeek-V3 splits a statement into subgoals, a 7B model proves each, and the composed proofs become training data, trading decomposability for data density; the RL reward is binary and comes from the Lean kernel. Vendor-reported: MiniF2F-test 88.9% at pass@8192, PutnamBench 49/658 (about 7.4%), own ProverBench 325 problems. Read them together: MiniF2F is near saturation at that budget while hard Putnam problems drop an order of magnitude, and ProverBench is self-built and self-run. The public repo (about 1304 stars) ships a ZIP of proofs you can run through Lean, putting verifiability a tier above closed models. Limits: pass@8192 means eight thousand-plus candidates per problem, not comparable with pass@1. Not commensurable with Kimina-Prover's 92.2%, so we list both without ranking. Graded C (vendor-stated): nothing recomputed in our own Lean 4 + mathlib environment.
- CONFIDENCE
- Vendor Claim
- Official model card or keynote only, no independent re-test
- KEY METRIC
- MiniF2F-test
- Vendor Claim · 2025-07
- MATURITY
- Research
- research → demo → product → production
Our takeWe grade it C (vendor claim). That looks contradictory next to "mathematics is mechanically verifiable", but it is not: what is verifiable is the proof text, not the 88.9%. The repository is public and the proofs are downloadable, so anyone with enough compute can check them; we simply have not done it, so we do not upgrade a number we never ran. Grade C here is honesty, not disparagement.
Its real contribution is the recursive subgoal decomposition cold-start route. RL for formal proving has long been stuck on sparse positives: a hard statement is not proved in one shot, so there is no reward to learn from. Having a strong model split the problem, a 7B model prove each subgoal, and then reassembling the complete proof converts a data-density problem into a decomposability problem, and that idea matters more to the field than this model's own score. The binary reward coming straight from the Lean kernel matters too - it makes reward hacking structurally hard on this route.
Read the gap, not the single point: the distance between MiniF2F at 88.9% and PutnamBench at 49/658 (about 7.4%) is the domain's true position - competition-level formal mathematics is close to saturation while genuinely hard problems remain in the single-digit percentages. Two more caveats: the pass@8192 budget means production cost is on the order of eight thousand generations, so comparing it to a pass@1 reading is invalid; and the error rate of autoformalisation (natural language to Lean statement) is not inside that 88.9%, even though in real use it is often the dominant source of failure.
The problem it solves: replacing "the model says it is correct" with "Lean says it is correct"
Mathematical reasoning is the hardest part of the AGI conversation to self-certify: when a model produces a proof, how do you know it is not plausible-sounding nonsense? DeepSeek-Prover-V2 takes the formal verification route - the output is not a natural-language chain of reasoning but Lean 4 code, checked line by line by the Lean kernel. If the checker accepts it, it is accepted; that layer depends on nobody's judgement, including the model's own confidence.
This is also the evidence form our confidence system values most, because mathematics is one of the few domains with formal ground truth. So even though the scores here are vendor-reported (we grade this C), the thing being reported is itself mechanically checkable, which is categorically different from "our model does better on our internal evaluation".
Model specs and training route
| Dimension | Reading | Why it matters |
|---|---|---|
| Scale and architecture | 671B MoE (shared lineage with DeepSeek-V3) | Not a small model ground out into a prover, but formal alignment on top of a flagship base |
| Target language | Lean 4 | The dominant proof assistant today, with the deepest library ecosystem (mathlib) |
| Cold-start data | DeepSeek-V3 performs recursive subgoal decomposition, then a 7B model proves each subgoal, synthesising training data | The core engineering advance over V1: hard problems are split into subproblems a small model can prove, then reassembled |
| Reinforcement learning | Binary reward (proof accepted / not accepted) | The reward signal comes from the Lean kernel rather than human preference, leaving no room to hack the reward into "looks right" |
| Availability | Public GitHub repository (about 1304 stars), including downloadable proof ZIPs | A step more verifiable than a closed model: the proof text can be run in Lean directly |
The recursive subgoal decomposition deserves expansion, because it is the crux of the whole route. Asking a model to prove a competition-level statement in one shot has a very low success rate, which leaves the RL stage with almost no positive samples to learn from. V2 instead has a strong model split the statement into a chain of subgoals and then has a 7B model prove each one - the subproblems pass far more often, so the reassembled complete proofs become high-quality training data. This is essentially trading decomposability for data density, a different cost structure from the AlphaProof approach of trading massive search for quality.
Benchmark readings (vendor-reported)
- MiniF2F-test: 88.9% (pass@8192). This is the most widely used public benchmark for formalised competition mathematics, and 88.9% sat in the top band of public readings as of 2025-07.
- PutnamBench: 49 / 658. Putnam problems are far harder than MiniF2F, and the denominator of 658 shows the board was still early; 49 solved was among the leading public readings at the time.
- ProverBench (self-built): 325 problems, including 15 from AIME 2024/2025. A self-built benchmark usefully covers problem types outside MiniF2F, but it is also the easiest place to overfit, so discount this number.
The right way to read the three together: MiniF2F at 88.9% says formalised competition mathematics is close to saturated under a pass@8192 sampling budget, while PutnamBench at 49/658 (about 7.4%) says capability drops an order of magnitude the moment the problems become genuinely hard. That gap is the real water level of formal proving today, and it carries more information than any single percentage.
Relation to the Kimina line
This site also catalogues Moonshot's Kimina-Prover. The two lines make quite different technical choices: Kimina starts from Qwen2.5-72B with RL and whole-proof generation (no intermediate prover feedback), and in 2025-07 pushed miniF2F to 92.2% with Kimina-Prover-72B; DeepSeek-Prover-V2 uses a 671B MoE with recursive subgoal decomposition cold start, reading 88.9%.
Comparing those two numbers directly requires great care: sampling budgets (pass@k) differ, miniF2F versions differ (Kimina also published a corrected version identifying at least five flawed problems in the original), and whether intermediate prover feedback is used differs. We therefore do not rank them against each other; we catalogue both side by side, precisely because the protocols are incommensurable. That is a direct consequence of this domain still having no unified third-party board: every reading is a lab's own run.
Boundaries
- pass@8192 is a very large sampling budget: it means generating more than eight thousand candidate proofs and filtering. The real production cost is that number, not a single call, and comparing it against a pass@1 reading is not valid.
- Formalising is not solving: it proves statements that have already been formalised. Turning a natural-language problem into a Lean statement (autoformalisation) is a separate step whose error rate is not included in the 88.9%.
- Deployment cost of a 671B MoE: even though activated parameters are far below total, self-hosting still needs many high-memory GPUs. Most teams can only use the API or reuse the published proofs.
- ProverBench is self-built: own problems, own run - structurally exposed to overfitting and selective reporting.
- Only covers formalisable mathematics: analysis, geometric intuition and modelling choices that resist Lean formalisation are outside the capability surface.
Our verification status
Facts come from the DeepSeek-Prover-V2 GitHub README (read in full, covering the training route, all three benchmark readings and the proof-ZIP release) and its technical report arXiv:2504.21801. The repository is public and the proof text is downloadable and independently checkable in Lean 4, which puts it a step above a closed model.
Confidence is nonetheless C (vendor claim), for a specific reason: we have not run these proofs. We have not downloaded the proof ZIPs, recomputed the 88.9% on MiniF2F-test against our own Lean 4 + mathlib environment, or independently recomputed PutnamBench's 49/658. Every benchmark number is vendor-reported, as are the sampling budget and the benchmark version. Reaching grade A would require: recomputing the MiniF2F-test pass rate and the actual sample count behind pass@8192 on a pinned Lean 4 + mathlib version, feeding every proof in the ZIP to the checker and counting real acceptances, and re-running on Kimina's corrected miniF2F so the two labs' readings become comparable.