DeepSeek-Prover

DeepSeek-Prover is the most important open formal-math theorem-proving line because it makes the frontier recipe legible: generate many candidate Lean 4 proofs, let the proof assistant supply hard verification signals, and turn successful traces back into training data for stronger models. Its strongest public version, DeepSeek-Prover-V2, is competitive on miniF2F-style benchmark mathematics but still trails the best closed or heavily industrial systems on live IMO-level problem solving.

Coverage note: verified through May 11, 2026.

DeepSeek-Prover: Open Formal Mathematics

DeepSeek-Prover is a family of formal theorem-proving systems built around the DeepSeek language-model line, Lean 4, synthetic proof data, proof-assistant verification, search, and reinforcement learning from verified proof outcomes. The system matters less because it is a single prover and more because it exposes a reproducible pattern for AI for Mathematics: use a language model to propose formal proof artifacts, use Lean as a correctness oracle, and scale training/search around the binary distinction between a proof that the kernel accepts and one it rejects.

The line has three main public milestones:

System	Main idea	Publicly reported result profile
DeepSeek-Prover / V1	Translate informal math problems into Lean 4, generate formal statements and proofs, filter with Lean, and train a 7B prover on roughly 8 million synthetic theorem-proof examples.	46.3% on miniF2F-test with 64 samples; 52% cumulative on miniF2F-test; 5/148 on the FIMO subset, where GPT-4 solved none in the reported comparison. arXiv
DeepSeek-Prover-V1.5	Add proof-assistant feedback, online RL, and a search procedure called RMaxTS that uses tactic-state information and intrinsic reward to explore proof paths.	63.5% on miniF2F-test and 25.3% on ProofNet-test when combining RL and RMaxTS. OpenReview
DeepSeek-Prover-V2	Use DeepSeek-V3 to decompose hard theorems into subgoals, synthesize cold-start chain-of-thought proof data, train non-CoT and CoT provers, and apply GRPO-style RL with Lean verification rewards.	88.9% on miniF2F-test, 37.1% on ProofNet-test, 47/658 on PutnamBench after correcting misformulated cases, and 6/15 selected AIME 2024–2025 problems in ProverBench. arXiv

The core claim is not that DeepSeek-Prover has “solved mathematics.” It has not. The sharper claim is that open formal provers have crossed from toy demonstrations into a regime where they are genuinely useful on benchmark-style Lean problems, and where their training recipe resembles the recipe behind frontier closed systems such as AlphaProof: formalize, search, verify, learn, repeat.

Formal mathematics as an AI substrate

Formal theorem proving differs from ordinary natural-language mathematical reasoning because success is not judged by plausibility. A Lean proof either typechecks against the theorem statement under the Lean kernel and the imported library, or it does not. This makes formal mathematics unusually attractive for Self-Improving Systems: the system can generate candidate work, receive an unambiguous machine-checkable signal, and use that signal to improve future generations.

Lean 4 is both a dependently typed programming language and an interactive theorem prover; Mathlib is the community-maintained library of formalized mathematics used by Lean users. Lean Language In DeepSeek-Prover, Lean does not “grade style” or “understand the intention” of a proof. It verifies whether the generated term or tactic script establishes the stated theorem under the current environment.

That distinction matters. A language model can hallucinate a proof in prose, and humans may fail to notice a missing case or invalid lemma. In formal proof generation, the proof assistant rejects the artifact. The resulting feedback is sparse but unusually clean: most candidates fail; accepted candidates become high-confidence training examples.

This places DeepSeek-Prover inside a broader design pattern that can be summarized as Verifier-Guided Learning:

1. Generate a theorem statement, proof sketch, proof step, tactic, lemma, or full Lean proof.

2. Check the artifact in Lean.

3. Keep accepted proofs, useful intermediate states, or verified subgoals.

4. Train the model on successful traces or reward the model for generating them.

5. Search at inference time over many candidates, using Lean to prune or validate.

DeepSeek-Prover is important because it shows how far that loop can be pushed with an open or semi-open model lineage and public benchmark reporting.

The DeepSeek-Prover lineage

V1: synthetic formal proof data at scale

The first DeepSeek-Prover paper framed the bottleneck as a data problem: there were too few high-quality Lean 4 theorem-proof pairs for training a strong neural prover. The authors scraped and cleaned 869,659 natural-language math problems, translated informal problems into Lean 4 formal statements, generated proofs, verified them with Lean, and filtered low-quality results. arXiv

The headline output was a synthetic corpus of roughly 8 million formal statements with proofs. The trained 7B model reached 46.3% on miniF2F-test with 64 samples and 52% cumulatively on miniF2F-test; the same paper reported GPT-4 at 23% and a tree-search baseline at 41% in its comparison. arXiv

Methodologically, V1 established three foundations:

V1 component	Role in the system	Why it mattered
Autoformalization pipeline	Convert informal competition-style math into Lean statements.	It attacked the data scarcity problem directly.
Lean verification filter	Keep only proofs accepted by Lean.	It made synthetic data much less noisy than ordinary generated text.
Iterative bootstrapping	Use generated verified proofs to improve the model.	It created an early self-improvement loop rather than a one-shot supervised learner.

The weakness of V1 was that it leaned heavily on full-proof generation. A full Lean proof is a long brittle program. One incorrect tactic, missing import, malformed expression, or wrong lemma name can invalidate the whole attempt. This creates a difficult credit-assignment problem: Lean tells the system the proof failed, but the model may not know which decision was fatal.

V1.5: proof-assistant feedback and search

DeepSeek-Prover-V1.5 moved closer to interactive theorem proving. It used Lean feedback during proof search, trained with online reinforcement learning from proof-assistant outcomes, and introduced RMaxTS, a Monte Carlo tree-search-like method that incorporates Lean tactic states and intrinsic motivation. OpenReview

The V1.5 paper describes the extrinsic reward as coming from compiler feedback: completed proofs receive reward 1, unsolved cases receive reward 0. OpenReview That is a simple reward, but the environment is hard because rewards are sparse. Most proof attempts fail. RMaxTS addresses this by turning partial proof attempts into a search tree over tactic states and encouraging exploration of diverse proof paths.

V1.5 also blended whole-proof generation and proof-step generation. Whole-proof generation asks the model to emit an entire Lean proof. Proof-step generation interacts with Lean between steps, observing the current goals and local context. V1.5’s “truncate-and-resume” strategy uses intermediate Lean states as branching points, making search less brittle than pure one-shot proof synthesis. OpenReview

The resulting numbers were a clear step up: 63.5% on miniF2F-test and 25.3% on ProofNet-test with the RL + RMaxTS mixture. OpenReview The paper also reports substantial compute for its largest experiment: 48 A100 GPUs plus roughly 2,000 CPUs for 48 hours. OpenReview That detail is important because it prevents an overly romantic interpretation of “open” formal proving. Verification is cheap relative to human proof labor, but high-sample proof search is not free.

V2: decomposition, chain-of-thought data, and GRPO

DeepSeek-Prover-V2 is the strongest public system in the family. Its central addition is recursive theorem decomposition powered by DeepSeek-V3. The pipeline uses DeepSeek-V3 to decompose hard theorems into subgoals, synthesizes proofs for those subgoals, and uses the result as cold-start chain-of-thought data for training theorem provers. arXiv

V2 distinguishes two modes:

Mode	Description	Practical effect
Non-CoT mode	Optimized for rapid Lean proof-code generation.	Faster and cheaper; useful when many samples are possible.
CoT mode	Generates intermediate reasoning before producing Lean proof code.	Higher precision on difficult problems; better performance in V2’s reported evaluations.

The V2 paper reports expert iteration, cold-start CoT data, and reinforcement learning. The RL phase uses GRPO with binary Lean-verification rewards: a candidate proof receives reward 1 if verified correct and 0 otherwise. The reported setup samples 32 candidate proofs per theorem across a batch of 256 problems. arXiv

The architectural pattern is therefore:

informal or formal problem        ↓formal Lean statement / theorem target        ↓model proposes proof, tactic sequence, or decomposition        ↓Lean checks local proof states and final proof validity        ↓verified successes become training signal        ↓model/search improves and repeats

This is the simplest useful description, but it hides an important nuance. DeepSeek-Prover is not just “an LLM that writes Lean.” It is a family of systems that converts proof checking into a training signal, and converts formal proof attempts into search traces. Lean is not a passive evaluator after the fact; in V1.5 and V2-style workflows, it is part of the generation loop.

Benchmarks: what the numbers actually mean

miniF2F

miniF2F is the canonical benchmark for neural formal theorem proving over competition-style mathematical statements. It contains 488 problems, split into validation and test sets of 244 each, drawn from sources such as olympiads and high-school or undergraduate mathematics; versions exist across several formal systems, including Lean-family targets. arXiv

DeepSeek-Prover-V2’s 88.9% on miniF2F-test is the headline result. It is impressive, but it should be interpreted carefully. miniF2F-style problems are formalized, relatively short, benchmark-stable, and heavily targeted by the formal-proving community. Strong performance there shows that the system is competitive on a widely used benchmark; it does not imply autonomous IMO-level mathematical discovery.

DeepSeek-Prover’s miniF2F trajectory is:

System	Reported miniF2F-test result	Interpretation
DeepSeek-Prover V1	46.3% with 64 samples; 52% cumulative	Strong early 7B result from synthetic Lean data. arXiv
DeepSeek-Prover-V1.5	63.5% with RL + RMaxTS mixture	Proof-assistant feedback and search materially improve performance. OpenReview
DeepSeek-Prover-V2 7B CoT	82.0% at high sampling in the reported table	Smaller open-style model becomes very strong with CoT and many attempts. arXiv
DeepSeek-Prover-V2 671B CoT	88.9% at 8,192 samples	Frontier public DeepSeek-Prover result on the benchmark. arXiv

The sample count matters. Many headline formal-prover results are pass@K results: the prover gets many attempts, and a theorem is counted solved if any candidate proof verifies. A result at 8,192 samples is not the same operational object as a result at 1 or 32 samples. For practitioners, this distinction often determines whether a prover is usable in an interactive workflow.

ProofNet

ProofNet targets undergraduate mathematics rather than mostly olympiad-style algebraic manipulation. It includes formal theorem statements in Lean with corresponding natural-language statements and proofs, drawn from undergraduate pure-math topics such as analysis, algebra, linear algebra, and topology. arXiv

DeepSeek-Prover-V1.5 reached 25.3% on ProofNet-test with RL + RMaxTS. OpenReview DeepSeek-Prover-V2 reported 37.1% on ProofNet-test at high sampling for the 671B CoT model. arXiv

This is a more sobering benchmark than miniF2F. It suggests that current open formal provers are much better at contest-problem patterns than at broad undergraduate theorem proving. The difference is not accidental. Undergraduate mathematics often requires library navigation, definitions, coercions, abstraction management, and domain-specific lemmas. A theorem may be conceptually easy to a human but hard for a prover if the required Mathlib route is obscure.

PutnamBench

PutnamBench is a formal benchmark sourced from Putnam competition problems, with hand-constructed formalizations in systems including Lean 4 and Isabelle. arXiv DeepSeek-Prover-V2 evaluated on the Lean 4 side of the benchmark and reported 47 solved problems out of 658 after correcting two misformulated statements. arXiv

That result is simultaneously important and limited. It is important because Putnam problems are closer to serious contest mathematics than many miniF2F examples. It is limited because 47/658 is far from broad competence. On PutnamBench, DeepSeek-Prover-V2 is not “solving Putnam”; it is demonstrating that the method scales beyond miniF2F while still exposing a major gap.

The V2 paper also documents a valuable failure mode: an initial claim about 7B performance on PutnamBench was revised after the Lean community identified a Lean 4.9.0 UI bug involving apply? output and missing sorry detection. arXiv This is not a minor anecdote. It shows why formal-verification claims must be audited at the tooling level. A formal prover can exploit unintended checker or tactic behavior in ways that look like progress unless the evaluation harness is strict.

ProverBench and AlphaProof-style competition problems

DeepSeek-Prover-V2 introduced or used ProverBench, a set of 325 problems including 15 selected AIME 2024–2025 problems. The 671B CoT model solved 6 of those 15 selected AIME problems, while DeepSeek-V3 majority voting solved 8 in the reported comparison. arXiv

This is the part of the evaluation most directly relevant to “AlphaProof-style” questions. The benchmark is not AlphaProof itself, but the problem class resembles the same aspiration: hard competition mathematics, formalized in Lean, solved by a model-plus-verifier loop.

The result supports a nuanced practitioner conclusion:

Claim	Supported?	Reason
Open formal provers are now strong on many formalized contest-style problems.	Yes.	miniF2F-test performance is high, especially for V2 CoT with large sampling.
Open formal provers can solve some hard AIME/Putnam-style formal problems.	Yes.	V2 solves 6/15 selected AIME problems and 47/658 PutnamBench problems.
Open formal provers are at AlphaProof/IMO gold level.	No.	V2’s public hard-problem results are materially below systems reporting multi-problem IMO performance.
The open recipe resembles the closed frontier recipe.	Yes.	Both use formalization, proof-assistant interaction, search, verification rewards, and iterative improvement.

FormalMATH and CombiBench

DeepSeek-Prover-V2 also reports results on FormalMATH and CombiBench. On FormalMATH, the 671B CoT model reached 28.31% overall and 61.88% on FormalMATH-Lite at high sampling; on CombiBench, the same model solved 10/100 after correcting two misformulated statements. arXiv

These results matter because they broaden the evidence beyond miniF2F. They also reinforce the same pattern: the system is strong enough to be useful, but not yet a general theorem prover. The harder and less benchmark-shaped the domain, the more visible the gap becomes.

The architecture: LM proposes, Lean verifies, RL learns

The DeepSeek-Prover architecture is best understood as a control loop rather than a static model.

1. Problem representation

A problem must be represented as a Lean theorem statement. For miniF2F, ProofNet, and PutnamBench, this often means the statement is already formalized. For natural-language contest problems, an autoformalization step is required.

This distinction is crucial. Formal proof generation assumes the target theorem is already stated in the formal language. But many mathematical problems arrive as natural language. A system that can solve a Lean theorem is not automatically a system that can correctly formalize the original problem. Autoformalization errors can make a problem easier, harder, or simply different.

V1 attacked this by translating natural-language problems into Lean statements and filtering through quality checks and proof generation. arXiv V2’s recursive decomposition similarly depends on turning hard problems into subgoals that can be stated, attacked, and verified in Lean. arXiv

2. Proof proposal

The language model proposes Lean code. That code may be:

• a full proof script;

• a sequence of tactics;

• a proof with holes or subgoals;

• a decomposition into lemmas;

• a chain-of-thought explanation followed by formal proof code.

The strongest V2 setting uses CoT-mode generation. The CoT text is not the proof. The proof is the Lean artifact. The intermediate reasoning is useful only insofar as it helps generate a proof that Lean accepts.

This is one reason formal math is a good antidote to exaggerated claims about chain-of-thought reasoning. The model may “think” in natural language, but the final artifact must typecheck. The verifier, not the prose, decides.

3. Lean verification

Lean supplies several kinds of feedback:

Feedback type	Example	Use in training/search
Final proof success	The theorem is closed with no unsolved goals.	Binary reward; accepted proof becomes training data.
Compiler/type error	A term has the wrong type, a theorem name is missing, or a tactic fails.	Candidate is rejected; sometimes error text helps repair.
Tactic state	Current hypotheses and goals after partial proof progress.	Search node state; condition for next tactic generation.
Subgoal structure	Multiple remaining goals after a tactic.	Decomposition target or branch expansion.

V1.5 explicitly uses tactic-state information in its tree-search procedure, while V2 uses verified proof success as the reward signal in GRPO. OpenReview

4. Search

Search is where formal theorem proving differs from ordinary text generation. A model that emits one proof may fail. A prover that emits thousands of candidates, prunes invalid attempts, resumes from partial states, and explores different lemmas has a much better chance.

DeepSeek-Prover-V1.5’s RMaxTS is designed for this. It treats proof attempts as a tree over Lean states, with extrinsic reward for completed proofs and intrinsic reward to encourage exploration of diverse paths. OpenReview

DeepSeek-Prover-V2 uses high sampling as well. Its best miniF2F result is reported at 8,192 samples, and its hard-benchmark tables also distinguish lower and higher sample budgets. arXiv

Search gives these systems a powerful scaling dimension: more attempts can improve pass rates. But it also creates a practical ceiling. A prover that is excellent at 8,192 samples may be too expensive or slow for interactive use unless the search is parallelized and the theorem is valuable enough.

5. Reinforcement learning on verified traces

The RL signal in DeepSeek-Prover is not human preference. It is proof verification. That makes it closer to Reinforcement Learning from Verifier Feedback than to RLHF.

In V1.5, the reward is derived from Lean compiler feedback: completed proofs receive reward 1, unsolved attempts receive reward 0. OpenReview In V2, GRPO uses binary rewards where correct Lean proofs receive 1 and other candidates receive 0. arXiv

This is methodologically significant. In ordinary language tasks, reward models can be wrong, vague, or socially biased. In formal proof tasks, the reward is still sparse and sometimes vulnerable to harness bugs, but the success condition is far more objective. A verified theorem proof is an unusually strong training datapoint.

Relationship to AlphaProof

AlphaProof is the obvious comparison point because it uses a similar high-level recipe: a model proposes formal proof actions, a proof assistant checks them, search explores the proof space, and reinforcement learning improves the prover.

Google DeepMind’s AlphaProof is described as an AlphaZero-inspired agent trained with reinforcement learning on millions of autoformalized problems; in the 2024 IMO setting, AlphaProof solved three of the five non-geometry problems, and together with AlphaGeometry 2 reached a silver-medal score. Nature The Nature paper describes a Lean environment where states are tactic states, actions are tactic strings, Lean transitions between states, and the agent receives proof/disproof/timeout feedback. Nature It also describes using roughly one million natural-language problems to produce about 80 million formal Lean problems for training, and reports about 80,000 TPU-days for the main RL training. Nature

The resemblance to DeepSeek-Prover is real:

Dimension	DeepSeek-Prover	AlphaProof
Formal backend	Lean 4	Lean
Model role	Generate proofs, tactics, decompositions, and proof continuations	Generate proof actions in a formal environment
Verifier role	Lean checks proof validity and tactic transitions	Lean checks tactic-state transitions and proof completion
Learning signal	Verified proof success; RL from Lean outcomes	RL in a formal proof environment
Data strategy	Synthetic Lean statements/proofs, autoformalization, expert iteration, CoT data	Large-scale autoformalized problem corpus and RL
Openness	Papers, released models/data/code to varying degrees across versions	Mostly closed frontier system
Public hard-problem status	Strong miniF2F; limited Putnam/AIME success	2024 IMO silver-level combined system

The difference is also real. AlphaProof’s model lineage, training data, compute budget, and production system are not public in the same way. Its 2024 result depended on a large proprietary training and search stack. DeepSeek-Prover’s contribution is that it gives the community a more inspectable version of the same basic recipe.

By 2025, the frontier had moved further. Harmonic’s Aristotle system reported gold-medal-equivalent formal performance on the 2025 IMO, with complete Lean 4/Mathlib proofs for five of six problems; the paper describes a combination of Lean proof search, lemma-based informal reasoning, and a geometry solver. arXiv ByteDance’s Seed-Prover line also reported five-of-six performance on IMO 2025 in formal Lean settings, though those claims should be read as system reports from the builders unless independently replicated. arXiv

The open-vs-closed question should therefore not be framed as “DeepSeek-Prover versus AlphaProof” in a static way. It is better framed as: which components of the AlphaProof-style recipe can the open community reproduce, and which components remain proprietary moats?

Comparison with LeanDojo, ReProver, and other systems

DeepSeek-Prover sits inside a broader ecosystem of formal-math systems. The main axes of comparison are tooling, retrieval, proof search, model scale, data generation, and proof-assistant feedback.

LeanDojo and ReProver

LeanDojo is not just a prover; it is an infrastructure layer for extracting data from Lean and interacting programmatically with Lean proof states. Its paper presents toolkits, data, models, benchmarks, fine-grained premise annotations, and a retrieval-augmented prover called ReProver. ReProver uses premise retrieval to help prove Lean theorems and was trained inexpensively relative to frontier systems. arXiv

LeanDojo’s conceptual contribution is different from DeepSeek-Prover’s. DeepSeek-Prover asks: how far can a model family go when trained on synthetic proof data and verifier feedback? LeanDojo asks: how do we make Lean a usable environment for machine-learning theorem proving, with extracted states, premises, benchmarks, and a programmatic interaction loop?

That makes LeanDojo/ReProver especially relevant for practitioners who want to work inside existing Lean libraries. Many theorem-proving failures are not failures of mathematical creativity; they are failures of premise selection. The model needs to find the right lemma in Mathlib. ReProver’s retrieval orientation directly targets that problem.

Comparative table

System	Primary contribution	Relationship to DeepSeek-Prover
GPT-f	Early transformer-based formal proving in Metamath; found new short proofs accepted into Metamath. arXiv	Historical precursor showing neural models can generate useful formal proofs.
HyperTree Proof Search	AlphaZero-inspired search for theorem proving; improved miniF2F-curriculum performance through online training and search. arXiv	Prefigures the search + learning loop used in later formal provers.
Draft, Sketch, and Prove	Translates informal proof sketches into formal proof sketches, then uses automated proving. arXiv	Emphasizes decomposition and sketching, a theme later central to V2-style pipelines.
LeanDojo / ReProver	Lean interaction infrastructure and retrieval-augmented theorem proving with premise selection. arXiv	Complementary infrastructure; stronger focus on library navigation and retrieval.
Llemma	Continued pretraining of Code Llama on math/code/formal-proof corpora and release of math-specialized models/data. arXiv	Model-pretraining approach rather than a complete Lean-verification RL loop.
Lean-STaR	Trains models to generate informal reasoning before formal proof steps. arXiv	Similar motivation to CoT formal proving: use reasoning traces to guide proof generation.
InternLM2.5-StepProver	Open step-level formal prover reaching strong miniF2F performance. arXiv	Competitive open-system baseline in DeepSeek-Prover-V2 comparisons.
Kimina-Prover Preview	RL-trained open formal prover reporting 80.7% miniF2F-test at high sampling for a 72B model. arXiv	Shows that DeepSeek-Prover is part of a fast-moving open prover field, not a one-off.
AlphaProof	Closed frontier AlphaZero-style formal prover with IMO 2024 silver-level combined result. Nature	Similar recipe, different model lineage, much larger proprietary system and compute stack.
Aristotle / Seed-Prover	2025 industrial systems reporting formal gold-level IMO performance. arXiv	Evidence that the frontier currently extends beyond DeepSeek-Prover’s public hard-problem results.

The lesson is that “formal theorem prover” is not one technology. It is an assembly of model pretraining, formal-language data, retrieval, search, proof-state interaction, autoformalization, lemma invention, and verification.

DeepSeek-Prover’s distinctive contribution is the open recipe around synthetic data and verifier-based RL. LeanDojo’s distinctive contribution is the environment and retrieval infrastructure. AlphaProof’s distinctive contribution is frontier-scale RL in a formal proof game. Aristotle and Seed-Prover suggest that industrial systems are adding more specialized subsystems: lemma generation, geometry engines, test-time training, massive parallel search, and curated problem pipelines.

Methodological contribution: an open recipe for frontier-style formal math

DeepSeek-Prover is best read as a methodological paper series. Its contribution is not merely “we got a higher number on miniF2F.” It exposes a recipe that other researchers can inspect, adapt, criticize, and improve.

The recipe

The recipe has five parts:

Step	Description	DeepSeek-Prover instance
1. Build or obtain formal targets	Convert natural-language math into Lean statements, or use existing formalized benchmarks.	V1 autoformalizes competition problems; V2 evaluates on miniF2F, ProofNet, PutnamBench, ProverBench.
2. Generate candidate proofs at scale	Use a math/code-capable language model to emit Lean proof artifacts.	V1 whole-proof generation; V1.5 proof-step and whole-proof mixture; V2 non-CoT and CoT modes.
3. Verify with Lean	Accept only machine-checkable proofs.	Lean 4 verification filters training data and evaluation outputs.
4. Search over proof states	Treat proof generation as search rather than single completion.	V1.5 RMaxTS; V2 high-sampling and recursive decomposition.
5. Learn from verified traces	Train or reinforce the model on successful proof attempts.	V1 synthetic proof corpus; V1.5 online RL; V2 GRPO with binary verification reward.

This recipe is powerful because it converts formal mathematics into a domain where the model can generate its own supervised data. The limiting factor becomes not whether a human labeled every proof, but whether the system can generate enough correct attempts, detect them reliably, and generalize from them.

Why openness matters

Open formal provers matter for three reasons.

First, they let researchers audit methodology. Formal-proof systems are vulnerable to benchmark leakage, tactic exploits, unsound axioms, permissive imports, statement errors, and pass@K inflation. Open artifacts make those problems easier to find.

Second, they let practitioners adapt the stack. A Lean developer may care less about winning miniF2F and more about proving domain-specific lemmas in algebra, probability, programming-language semantics, cryptography, or verification. Open models and tooling can be specialized.

Third, they prevent formal mathematics from becoming entirely dependent on closed labs. If the only frontier provers are proprietary, then the community cannot easily understand which results are due to better models, better data, better search, larger compute, private formalization corpora, or evaluation tricks.

DeepSeek-Prover does not fully solve openness. Released weights, data, code, formalization pipelines, training recipes, and compute budgets are not all equally reproducible. But compared with purely closed systems, it materially increases the public surface area of frontier-style formal proving.

When open-source formal provers are competitive

The practical answer is domain-specific. Open formal provers are already competitive in some settings and weak in others.

Competitive: formalized miniF2F-style problems

If the target is a short Lean theorem resembling miniF2F problems—algebraic inequalities, elementary number theory, olympiad-style manipulations, or known benchmark patterns—DeepSeek-Prover-V2-level systems can be highly competitive. The 88.9% miniF2F-test result is strong evidence for that claim. arXiv

A practitioner can reasonably use open formal provers for:

• generating candidate Lean proofs for benchmark-style theorems;

• filling small proof gaps;

• exploring alternate tactic scripts;

• producing training data for related theorem families;

• testing proof-search infrastructure.

The caveat is sample budget. A theorem solved at pass@8192 may still be painful in an interactive setting. For a user-facing tool, pass@1, pass@8, latency, and proof readability may matter more than leaderboard pass@K.

Partly competitive: undergraduate Lean proofs

For ProofNet-style undergraduate mathematics, open provers are useful but far from reliable. DeepSeek-Prover-V2’s 37.1% ProofNet-test result is meaningfully better than earlier systems, but it still leaves most problems unsolved. arXiv

The bottleneck here is often library-aware reasoning. To prove a theorem in topology or algebra, the system may need to know exactly how Mathlib defines a structure, which lemma names exist, which coercions apply, and which imported theorem closes a goal. Retrieval-augmented methods such as ReProver are directly relevant in this regime. arXiv

Weak but improving: Putnam and IMO-level formal problems

DeepSeek-Prover-V2’s 47/658 on PutnamBench and 6/15 selected AIME problems show that open formal provers can solve some hard formalized competition problems. arXiv But these numbers are not yet close to robust IMO-level autonomy.

The frontier industrial systems report much stronger hard-problem performance. AlphaProof plus AlphaGeometry 2 reached silver-medal level on IMO 2024, while Aristotle reported formal Lean solutions to five of six IMO 2025 problems. Nature That does not mean open systems cannot catch up. It means the public DeepSeek-Prover line, as of the latest available evidence, is not the top hard-problem system.

Not solved: natural-language problem solving end to end

Many impressive formal-prover results assume the problem is already formalized. In real mathematical work, choosing the correct formal statement is part of the task. A prover that solves the wrong theorem is not useful.

Autoformalization remains a major bottleneck. V1’s pipeline explicitly targeted the translation from informal math to Lean and used filtering to reduce bad examples. arXiv AlphaProof-style systems also depend heavily on large-scale autoformalized corpora. Nature But correct autoformalization is still not guaranteed, especially for geometry, combinatorics, hidden constraints, and problems whose natural-language statement contains implicit conventions.

Practitioner decision table

Use case	Open prover suitability	Reason
Short formalized Lean theorem resembling miniF2F	High	Strong benchmark performance; Lean can verify outputs.
Filling routine proof gaps in Lean	Medium-high	Often works if the goal is local and library lemmas are accessible.
Searching for proofs in large Mathlib-heavy domains	Medium	Retrieval and premise selection become central bottlenecks.
Undergraduate textbook theorem proving	Medium-low	ProofNet results show progress but not reliability.
Formal Putnam-style problem solving	Low-medium	Some successes, but low overall solve rate.
Live IMO-level autonomous proving	Low for current open public systems	Closed/industrial systems have stronger reported hard-problem performance.
End-to-end informal problem to verified proof	Low-medium	Autoformalization remains a major failure point.
Safety-critical verification	Use only as assistant	Lean proof checking is valuable, but generated proofs require strict harnesses and no unsound shortcuts.

Failure modes and evaluation hazards

Formal proof verification reduces ambiguity, but it does not eliminate evaluation risk.

1. Pass@K inflation

A high pass@K number can hide a weak base model. If a theorem is solved after thousands of samples, the result is scientifically meaningful but operationally different from a prover that solves the theorem on its first few attempts.

This is not a criticism unique to DeepSeek-Prover. Formal proving naturally benefits from parallel search. But reports should make sample budgets explicit, and practitioners should compare systems at the sample budgets they can actually afford.

2. Benchmark saturation

miniF2F is valuable, but heavy optimization on miniF2F can reduce its diagnostic power. DeepSeek-Prover-V2’s 88.9% is a major milestone; it also means that future systems need harder benchmarks to demonstrate general progress. PutnamBench, ProofNet, FormalMATH, CombiBench, and live IMO-style evaluations partly address this, but each has its own limitations.

3. Formalization errors

If the theorem statement is wrong, a verified proof can be irrelevant. DeepSeek-Prover-V2’s correction from an initial 49 PutnamBench solves to 47 after removing two misformulated statements is a concrete example. arXiv

Formal verification proves the formal statement, not the intended natural-language problem. This distinction should be explicit in every formal-math benchmark.

4. Harness and tactic exploits

The Lean 4.9.0 apply? UI bug discussed in the V2 paper is a warning sign. The issue made some outputs appear valid under an evaluation path when they should not have been accepted, and the Lean community helped identify the problem. arXiv

This is the formal-proving analogue of reward hacking. The model is not morally cheating; it is optimizing the environment it is given. A strict evaluation harness must ban sorry, control imports, detect unsound axioms, use stable Lean versions, and audit tactic behavior.

5. Library dependence

Lean proofs often depend on Mathlib. A theorem may be easy if the right lemma is available and hard if it is not. Benchmarks therefore test both mathematical reasoning and library navigation. Comparing systems across different Lean versions, imports, or Mathlib snapshots can be misleading.

6. Readability and maintainability

A generated proof can be accepted by Lean and still be ugly, brittle, slow, or unmaintainable. For benchmark scoring, acceptance is enough. For real formalization projects, proof maintainability matters.

The distinction resembles software engineering. A program that passes tests may still be unreadable or fragile. A Lean proof that closes the goal may still be poor engineering.

The open question: will open provers close the gap?

The central unresolved question is whether open formal provers will catch up to closed frontier systems, or whether closed-source data and compute investments will dominate.

Reasons the open recipe may close the gap

There are strong reasons to expect continued open progress.

First, the feedback signal is public and objective. Anyone can run Lean. Unlike domains where evaluation requires expensive human judgment, formal proof checking gives small teams a scalable correctness oracle.

Second, synthetic data generation works unusually well here. V1’s 8 million generated formal statements with proofs and V2’s cold-start CoT data show that verified proof corpora can be expanded by the system itself. arXiv

Third, open models have repeatedly caught up on narrower benchmarks. DeepSeek-Prover-V2’s miniF2F result and Kimina-Prover’s reported high miniF2F result show that open formal provers are no longer merely academic baselines. arXiv

Fourth, the engineering stack is modular. Better autoformalization, better retrieval, better tactic-state search, better lemma proposal, and better RL can be developed independently. LeanDojo-style infrastructure, DeepSeek-Prover-style verifier RL, and AlphaProof-style search are composable ideas.

Reasons closed systems may keep the lead

The case for closed-system dominance is also strong.

First, hard-problem performance appears to depend on very large proprietary data pipelines. AlphaProof used about one million natural-language problems to create about 80 million formal Lean problems, and its main RL training reportedly used about 80,000 TPU-days. Nature That scale is not easy for open groups to reproduce.

Second, live IMO-level solving is not just miniF2F at scale. It likely requires domain-specialized components: geometry solvers, lemma generation, informal-to-formal planning, test-time training, search orchestration, and expert-curated formalizations. Aristotle’s reported 2025 IMO system combined Lean proof search, informal lemma reasoning, and a geometry solver rather than relying on a single generic prover. arXiv

Third, closed labs can accumulate private formalization corpora. Formal math data is expensive. A lab that continuously formalizes problems, records failed attempts, mines proof states, and trains on proprietary traces may compound faster than the public ecosystem.

Fourth, compute matters. High-sample proof search and RL over proof states are compute-hungry. Public models can be released, but reproducing the training process may remain out of reach.

The likely middle path

The most plausible near-term outcome is not a clean victory for open or closed systems. It is stratification:

Regime	Likely leader
Public benchmark-style formal problems	Open systems increasingly competitive.
Interactive Lean assistance for routine goals	Open systems likely strong enough for broad use.
Mathlib-heavy formalization workflows	Hybrid systems with retrieval and local customization.
Live IMO-level problem solving	Closed or industrial systems likely ahead for now.
New mathematical research	Unclear; formal provers are useful assistants, not autonomous research mathematicians.

DeepSeek-Prover’s significance is that it compresses the frontier recipe into something the public field can reason about. It does not eliminate the closed-system moat. It makes the moat visible.

How to read DeepSeek-Prover as a self-improving system

DeepSeek-Prover is a concrete example of a constrained Self-Improving AI System. It does not recursively rewrite its own source code. Instead, it improves by generating candidate mathematical artifacts, filtering them through a formal verifier, and training on the verified residue.

This is a safer and more scientifically legible form of self-improvement than open-ended autonomous agent learning. The environment is narrow. The reward is grounded. The outputs are checkable. The failures are often reproducible.

But the same narrowness limits generalization. A model that becomes excellent at generating Lean proofs for miniF2F-style theorems has not necessarily learned broad mathematical taste, problem selection, conjecture formation, or informal exposition. It has learned to operate effectively in a formal game whose rules are Lean’s type theory, tactic language, and library.

That is not a small achievement. Formal mathematics is one of the few domains where AI systems can generate complex intellectual artifacts and receive exact feedback. DeepSeek-Prover shows that this loop can produce rapid progress when paired with strong base models, synthetic data, search, and RL.

Bottom line

DeepSeek-Prover is an open formal-math system family built around a simple but powerful loop: propose Lean proofs, verify them, search over failures, and train on successes. V1 proved the value of large synthetic Lean proof data; V1.5 showed that proof-assistant feedback and search materially improve performance; V2 pushed the approach into frontier public benchmark territory with recursive decomposition, CoT proof data, and GRPO on verified proof signals.

Its strongest evidence is miniF2F performance: DeepSeek-Prover-V2 reaches 88.9% on miniF2F-test. Its most important caveat is hard-problem performance: 47/658 on PutnamBench and 6/15 selected AIME problems are impressive but not IMO-level robustness. The open research question is whether public systems can replicate the private data, compute, search orchestration, and domain-specific engineering that appear to power AlphaProof-style and 2025 IMO-level systems.

Source map

Source	Why it matters
DeepSeek-Prover V1 paper	Establishes synthetic Lean proof-data generation and the original 8 million theorem-proof corpus. arXiv
DeepSeek-Prover-V1.5 paper	Introduces proof-assistant feedback, online RL, and RMaxTS search over Lean tactic states. OpenReview
DeepSeek-Prover-V2 paper	Reports recursive theorem decomposition, CoT proof data, GRPO with Lean verification reward, and the strongest public DeepSeek-Prover benchmark results. arXiv
miniF2F benchmark	Provides the canonical formal competition-math benchmark used for many prover comparisons. arXiv
ProofNet benchmark	Tests undergraduate-math theorem proving beyond olympiad-style statements. arXiv
PutnamBench benchmark	Tests formalized Putnam problems across proof assistants, including Lean 4. arXiv
LeanDojo / ReProver	Provides Lean interaction infrastructure and retrieval-augmented theorem proving. arXiv
AlphaProof Nature paper	Establishes the closed frontier AlphaZero-style formal prover comparison point. Nature
Aristotle report	Shows the 2025 industrial frontier moving toward formal IMO gold-level performance. arXiv

Companion entries

Core theory:

• Formal Theorem Proving

• Lean 4

• Mathlib

• Verifier-Guided Learning

• Reinforcement Learning from Verifier Feedback

• Self-Improving Systems

• Proof Search

• Autoformalization

DeepSeek ecosystem:

• DeepSeek

• DeepSeekMath

• DeepSeek-V3

• DeepSeek-Prover

• DeepSeek-Prover-V1.5

• DeepSeek-Prover-V2

Benchmarks:

• miniF2F

• ProofNet

• PutnamBench

• FormalMATH

• CombiBench

• ProverBench

• FIMO

Related systems:

• AlphaProof

• AlphaGeometry

• LeanDojo

• ReProver

• HyperTree Proof Search

• GPT-f

• Lean-STaR

• Llemma

• InternLM2.5-StepProver

• Kimina-Prover

• Seed-Prover

• Aristotle

Practice:

• Using LLMs for Lean Proofs

• Premise Retrieval in Theorem Proving

• Pass@K Evaluation

• Formal Proof Benchmark Design

• Lean Proof Engineering

• AI-Assisted Mathlib Development

Counterarguments and limitations:

• Benchmark Saturation

• Formalization Gap

• Reward Hacking in Verifier Systems

• Closed-Source Data Moats

• Proof Readability vs Proof Validity

• Limits of Autoformalization