DeepSeek-Prover

TL;DR#

• What was built: DeepSeek-Prover, a 7B model initialized from DeepSeekMath-Base 7B that writes complete Lean 4 proofs in one pass, with no step-by-step interaction with the proof checker (§3, §4.1).
• Key idea: formal proof data is scarce, so make it. Translate 869,659 informal math problems into Lean 4 statements (autoformalization), throw out trivial or self-contradictory ones, try to prove each statement and its negation, keep whatever the Lean checker accepts, retrain, repeat (§3, Figure 1).
• Scale: 712,073 statements survive filtering (§3.2). Over the iterations this yields about 8 million statement–proof pairs (8,066,621 in Table 5).
• Headline result: 46.3% on miniF2F-test at pass@64, against 23.0% for GPT-4-turbo. Pooling all runs gives 52.0% on test and 60.2% on validation, ahead of Hypertree Proof Search at 41.0% on test (Table 1).
• Hard problems: proves 5 of the FIMO IMO-shortlist problems; GPT-4 proves none (§4.2).
• Ablations: each round of self-training improves the score (34.0% → 46.3% on test over 5 iterations, Table 4). Accuracy keeps rising as the synthetic set grows by factors of 10, up to 8M examples (Table 5).

Why it matters#

A proof in Lean either compiles or it doesn't. That makes formal theorem proving one of the few reasoning tasks where a model's output can be checked automatically and with no doubt. The catch is data. Few people write Lean, so there is far less of it than Python. Lean's main library, mathlib, gives only 0.238B tokens of proof data in this paper's setup (Table 2). Earlier neural provers made up for weak models with heavy search: GPT-f, Proof Artifact Co-Training and Hypertree Proof Search call the checker after every proof step and search a large tree. That costs a lot of compute and still topped out around 41% on miniF2F-test (Table 1).

DeepSeek-Prover takes the other route: build a much larger training set and keep inference simple. The idea is the expert-iteration loop from GPT-f, with one change. The loop runs on statements the model has autoformalized from web-scraped problems, not on a fixed human-written set. Every proof is checked by Lean, so the data is correct by construction, though a statement may still say something other than the original problem meant. The paper's engineering goes into two weak points of that pipeline. It filters out bad statements, and it avoids wasting compute on statements that are false.

Key idea A proof checker turns a weak model's lucky successes into perfectly labelled training data. Generate many candidate theorems, let Lean keep only the proofs that check out, retrain, and the model's success rate grows round after round.

In the DeepSeek arc, this paper sits between DeepSeekMath, which provides the base model and the math pre-training, and DeepSeek-Prover-V1.5. V1.5 reuses this synthetic dataset, adds reinforcement learning with the Lean checker as reward (using GRPO from DeepSeekMath), and adds a tree search. The pattern seen here, where a verifier supplies the labels and the model trains on its own checked outputs, appears again in DeepSeek's later reasoning work.

Background you need#

• Lean 4 and formal proofs. Lean is a programming language and proof assistant. A theorem is written as a typed declaration, for example theorem foo (x : ℝ) (h₀ : 0 < x) : 0 < x ^ 2. The parts before the colon are hypotheses. The part after it is the goal. A proof is code that Lean's kernel checks. If it compiles with no errors, the theorem is proved and no human review is needed.
• Tactics and tactic states. Most Lean proofs are written in tactic mode, which starts after := by. Each tactic, such as intro, simp, linarith or nlinarith, changes the current proof state: the list of hypotheses plus the remaining goal, shown as ⊢ goal. When no goals are left, the proof is done. linarith and nlinarith are automated tactics for linear and nonlinear arithmetic. Much of this paper's model output is a few calls to powerful tactics like these (Appendix A.3).
• Mathlib. Lean's large community math library of definitions and lemmas, such as Real.sqrt, Nat.choose and Matrix.det. Every generated proof is checked against a fixed mathlib commit with a long list of imports (Appendix A.4).
• Autoformalization. Translating a natural-language math statement into a formal one (Wu et al., 2022). The hard part is faithfulness. A translation can type-check and still state a different, easier or even contradictory theorem.
• Whole-proof vs. proof-step generation. Proof-step provers generate one tactic, ask Lean for the new state, and search over a tree of states. Whole-proof provers write the full proof in one go and only then check it. DeepSeek-Prover is whole-proof, which is simple and cheap per sample but gives no feedback partway through a proof.
• pass@k and expert iteration. pass@k is the fraction of problems for which at least one of k sampled proofs verifies. Expert iteration (Polu & Sutskever, 2020) repeats a loop: sample proofs, keep the verified ones, fine-tune on them, and sample again.

The core ideas#

The pipeline has five stages (Figure 1): autoformalize, filter, prove, fine-tune, repeat. One model, DeepSeek-Prover, plays every role: translator, quality grader, and prover.

1. Autoformalization at scale#

The authors scraped and cleaned 869,659 natural-language problems from high-school and undergraduate exercises, exams and competitions (§3.1). They chose this level on purpose. These problems have explicit conditions and clear goals, so they are easier to formalize than research mathematics, which needs elaborate definitions. The set leans toward algebra and number theory, with less combinatorics, geometry and statistics.

DeepSeekMath-Base 7B could not formalize problems well on its own. So it was first fine-tuned on MMA (Jiang et al., 2023), a dataset of mathlib statements back-translated into English by GPT-4. Fine-tuning on it in the reverse direction teaches English-to-Lean translation. The prompt is minimal (§3.1):

Mathematical Problem in Natural Language:
{informal_statement_with_answers}
Translate the problem to Lean 4 (only the core declaration):
```lean4

The output is only the theorem statement. It has no proof yet.

2. Quality filtering: model scoring and hypothesis rejection#

Raw autoformalizations have two common failure modes (§3.2).

Too easy. Many statements are trivial. The model grades each statement with a chain-of-thought prompt, using miniF2F-valid examples as few-shot demonstrations and criteria such as complexity, depth and relevance (prompt in Appendix A.1). Grades are "excellent", "good", "above average", "fair" or "poor". The authors drop "fair" and "poor" and report that a manual check agreed with the grades.

Vacuous. A statement whose hypotheses contradict each other is trivially "provable", because from a false premise anything follows. The paper's example has the hypothesis

which fails for \(z=1\). To catch such cases, hypothesis rejection keeps the hypotheses, replaces the goal with False, and asks the prover to prove that. Here the proof is a single tactic, simpa using h0 1. If False can be proved, the hypotheses are inconsistent and the statement is discarded.

Together these filters leave 712,073 statements.

3. Proving a statement and its negation in parallel#

Even after filtering, the authors estimate that at least 20% of statements are false (§3.3). Often the translation itself is wrong. A brute-force prover would spend its whole sampling budget on each of them before giving up, since no proof of a false statement can exist.

The fix uses a basic fact of logic. For hypotheses \(\Gamma\) and claim \(P\), run two proof searches at the same time:

Here \(\vdash\) means "proves". Each search tries up to \(k\) samples, and both stop as soon as either one succeeds. A proof of \(\neg P\) settles the question quickly and frees the compute. It is also useful data: a correct, verified theorem–proof pair, even though the theorem is the negation of what the translator meant. The paper calls this a form of data augmentation. All verified proofs, of \(P\) or of \(\neg P\), go into the training set.

A worked example of why this matters: section 5.2 shows a determinant problem that was mistranslated with a universal quantifier, "for all nonzero \(a,b,c\), \(\det(\ldots)=D\)". The model instances the hypothesis at \((1,2,3)\) and at \((1,4,9)\), which give different determinants, and derives False with linarith.

4. Iterative enhancement#

The pipeline depends entirely on DeepSeek-Prover, so improving the model improves every stage. After each round, the model is fine-tuned on all verified theorem–proof pairs so far. The improved model then autoformalizes, scores and proves again. The loop stops when gains become marginal (§3.4). The model learns from its own verified successes: Lean filters out every wrong proof, so the training labels never get noisier, even as the model takes on harder statements.

Table 4 shows the effect on miniF2F at pass@128: test accuracy goes 34.0% → 39.3% → 41.4% → 45.1% → 46.3% across iterations 0–4.

5. Training and inference#

Fine-tuning settings (§4.1): DeepSeekMath-Base 7B, which was pre-trained on 120B math-related tokens; global batch size 512; constant learning rate \(1\times10^{-4}\); 6,000 warm-up steps. Lean version v4.7.0-rc2 with a pinned mathlib commit (footnotes in §3).

Inference is plain sampling. The model writes a whole proof, Lean checks it, and pass@k counts a problem as solved if any of k samples checks. There is no search tree and no step-by-step interaction with Lean. That is why the comparison in Table 1 is interesting: a 7B model sampling whole proofs beats systems that run thousands of checker-guided expansions.

What the proofs look like#

The appendix examples are short. Typically the model sets up a few have facts and finishes with nlinarith, linarith, field_simp or simp_all (Appendix A.3). Bernoulli's inequality, for instance, is proved by induction' followed by simp_all [...] and nlinarith [mul_self_nonneg (1 + x - 1)]. In other words, much of the model's skill lies in choosing which automated tactic to call and which hints to give it. V1.5 later names this as a weakness and adds natural-language reasoning as comments.

Key numbers#

How to read the paper#

The main body is about 10 pages and easy to read. The appendix is mostly Lean code, worth skimming if you have never seen Lean.

• Abstract and §1 Introduction — Read closely. States the full pipeline and the two concerns, "quality assurance" and "scale assurance". The negation trick is introduced here.
• §2 Background and Related Works — Skim. A short survey of tree-search provers, whole-proof provers and autoformalization. Useful for knowing the names in Table 1.
• §3 Approach — Read closely. The core of the paper. Look at Figure 1 first. §3.2 (scoring and hypothesis rejection) and §3.3 (proving the negation in parallel) are the two clever parts. §3.4 is one paragraph.
• §4.1 Experimental Setup — Skim. Training hyperparameters and baselines.
• §4.2 Main Results — Read closely. Table 1 is the key result. Note how "generation times" is counted differently for tree search (for example 64 × 5000) and for whole-proof sampling, and note that "cumulative" pools many runs.
• §4.3 Ablations — Read closely. Tables 2–5 each answer one question: is autoformalized data better than mathlib, does the quality filter help, does iterating help, does scale help? They are short and carry most of the evidence.
• §5 Case Studies — Read. Two short examples: a faithful formalization, and an inconsistent one caught by hypothesis rejection.
• §6 Conclusion and Broader Impact — Skim.
• Appendix A.1 (scoring prompt) — Skim. The grading criteria, such as "relevance to current research" and "interdisciplinary potential", are rather loose for competition problems.
• Appendix A.2–A.3 (example proofs) — Skim on first pass. Read 2–3 proofs to see the style.
• Appendix A.4 (imports) — Skip.

Suggested order: Figure 1 → §3 → Table 1 → Tables 2–5 → §5 → skim the appendix proofs. About 45–60 minutes, or longer if you stop to understand the Lean examples.

Check your understanding#

Limitations and open questions#

• Domain coverage. The authors note that the work mainly covers algebra and number theory at the high-school and undergraduate level (§6). Geometry and combinatorics are hard to formalize in Lean and are underrepresented.
• Statement fidelity isn't measured. Lean guarantees that a proof proves the formal statement, not that the statement matches the original problem. Some appendix examples look looser than the English problem. The FIMO 2009 functional equation is stated over ℕ with 0, not positive integers, and the proof leans on f 0 = 0. The paper gives no faithfulness evaluation.
• The quality score is a rough proxy. The grading prompt asks about "relevance to current research" and "interdisciplinary potential", which say little about competition problems. Table 3 shows the filter helps by about 4.5 points, but not why.
• Numbers that are hard to reconcile. Table 4 (iteration 4) reports 46.3% on test at pass@128, while Table 5 (full 8M set) reports 40.16%. The setups probably differ, but the paper does not explain how. The FIMO benchmark is described as having 148 problems in the abstract and 149 in §4.2. "Cumulative" in Table 1 pools runs without a precise definition, so 52.0% is not a pass@k at a fixed k.
• How 712k statements become 8M pairs is not spelled out. Presumably the count includes several proofs per statement, negation proofs and later iterations, but the paper does not break it down.
• Possible benchmark contamination. The scraped web problems include competitions such as AMC, AIME and IMO, which are also miniF2F's sources. The paper does not describe decontamination against miniF2F or FIMO.
• Released data. The paper promises to release the dataset. The public Hugging Face release (deepseek-ai/DeepSeek-Prover-V1) is tagged in the 10K–100K size range, so it appears to be a subset, not the full 8M.

Further reading#

• DeepSeek-Prover-V1.5: the direct sequel. Reuses this data, adds RL from Lean feedback and a tree search, and reaches 63.5% on miniF2F-test.
• DeepSeekMath: the base model and its math pre-training corpus, and the source of GRPO, which V1.5 uses.
• DeepSeek-Coder: the code-model lineage that DeepSeekMath was initialized from.
• Polu & Sutskever, Generative Language Modeling for Automated Theorem Proving (GPT-f): arXiv:2009.03393
• Polu et al., Formal Mathematics Statement Curriculum Learning (expert iteration in Lean): arXiv:2202.01344
• Lample et al., HyperTree Proof Search for Neural Theorem Proving: arXiv:2205.11491
• Wu et al., Autoformalization with Large Language Models: arXiv:2205.12615
• Jiang et al., Draft, Sketch, and Prove: arXiv:2210.12283
• Zheng et al., miniF2F: arXiv:2109.00110; Liu et al., FIMO: arXiv:2309.04295
• Model and data: deepseek-ai/DeepSeek-Prover-V1 on Hugging Face
• Later, outside this series: DeepSeek-Prover-V2 (2025), arXiv:2504.21801