DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

ArXiv: 2405.14333

🎯 Pitch

A 7B model, fine-tuned on 8 million autoformalized competition problems and iteratively refined on its own proofs, outperforms GPT-4 on formal theorem proving—solving Olympiad problems where GPT-4 scores zero. The key is a self-improvement loop that generates, filters, and proves statements at massive scale, overcoming the extreme data scarcity that has capped neural provers.

1. Executive Summary

This paper introduces an iterative method to synthesize extensive Lean 4 proof data from a corpus of 869,659 high-school and undergraduate mathematical competition problems, addressing the critical bottleneck of scarce training data in formal theorem proving. The approach integrates large-scale autoformalization (translating natural language problems into formal statements via an LLM fine-tuned on back-translated mathlib data), quality filtering (model-based scoring of statement complexity combined with a hypothesis rejection strategy that proves the negation of potentially inconsistent hypotheses to prune unprovable statements), and iterative self-improvement (fine-tuning the DeepSeekMath-Base 7B model on validated theorem-proof pairs and cycling the improved model back through the pipeline). Trained on the resulting dataset of 8 million formal statement-proof pairs, DeepSeek-Prover achieves 46.3% whole-proof generation accuracy at 64 samples and 52% cumulative pass rate on the Lean 4 miniF2F test set, outperforming GPT-4's 23.0% at 64 samples and a tree search reinforcement learning method at 41.0%, while also solving 5 out of 148 FIMO problems—a benchmark where GPT-4 solves zero—establishing that large-scale synthetic data can substantially advance neural theorem proving when the model is iteratively refined on its own verified outputs.

2. Context and Motivation

The Core Problem: Automated Theorem Proving Is Data-Starved

The fundamental challenge this paper tackles is the scarcity of training data for neural theorem provers. Formal proof assistants like Lean, Isabelle, and Coq have revolutionized mathematical verification by providing mechanical, fully rigorous checking of proofs — eliminating the possibility of hidden errors that plague human peer review. Since the introduction of these systems, mathematicians have formalized significant bodies of mathematics, but the process remains labor-intensive, requiring specialized expertise and years of effort even for routine material (the paper notes that crafting formal proofs "demands significant effort, specialized expertise, and poses challenges even for seasoned mathematicians" — Section 1, paragraph 2).

Large language models (LLMs) have recently emerged as a promising vehicle for automating parts of this process. Pre-trained on massive code and mathematics corpora, models can generate candidate proof steps, suggest tactics, or even produce entire proofs in a single pass. However, their effectiveness is gated by the amount of parallel data — pairs of natural language mathematical statements and their corresponding formal proofs in the target proof assistant language (Section 1, paragraph 3):

"Unlike conventional programming languages such as Python or Java, formal proof languages are used by relatively few mathematicians, resulting in limited datasets."

This is not merely a "nice-to-have" data problem. The underlying mathematics is genuinely sparse as formalized content. Mathlib, the standard library for Lean 4, contains thousands of theorems, but these represent hand-curated proofs painstakingly written by a small community over many years. The total volume of formal proof data available for training is orders of magnitude smaller than what is available for conventional programming languages, where repositories like GitHub provide billions of lines of code. In this regime, even state-of-the-art models are far from achieving practical utility on complex mathematical problems — the pass rates on competitive benchmarks like miniF2F and FIMO remain low, and the search spaces for theorems of IMO-level difficulty are too vast for pure search-based approaches to navigate efficiently.

Why This Problem Matters: Beyond Peer Review

The paper's motivation extends beyond the immediate goal of building a better theorem prover. The importance of automated or semi-automated formal proof generation has several dimensions:

Reliability of mathematical knowledge. The paper opens with a pointed observation: "the increasing complexity of proofs presents substantial challenges for peer review. This complexity has led to the acceptance of erroneous proofs, with critical flaws often detected only after considerable time" (Section 1, paragraph 1). This is not hypothetical — mathematics has witnessed several high-profile cases where accepted proofs were later found to contain unfixable gaps, sometimes decades after publication. Formal verification provides a definitive answer to the question "is this proof correct?" but only if the proof has been formalized. Making formalization easier directly lowers the barrier to producing machine-checkable mathematics.

Democratization of formal methods. As the paper notes, crafting formal proofs "demands significant effort, specialized expertise, and poses challenges even for seasoned mathematicians" (Section 1). If LLMs can assist with or fully automate large portions of the formalization process, mathematicians without specialized training in proof assistants could produce verified mathematics. The downstream impact on fields like cryptography, hardware verification, and safety-critical software — all of which rely on formal guarantees — could be substantial.

Training data as the bottleneck, not model capability. An implicit but important motivation in the paper is the recognition that model architecture and scale are not the primary constraints on neural theorem proving today. DeepSeekMath-Base 7B, the foundation model used in this work, already demonstrates strong mathematical reasoning capabilities from its pretraining on 120 billion math-related tokens (Section 4.1). The gap between what this model could learn and what it does learn comes down to the availability of high-quality, domain-specific supervised data — formal statements paired with verified proofs. The paper's core thesis is therefore that data generation, not model scaling, is the critical path to advancing neural theorem proving.

Prior Approaches and Where They Fall Short

The paper identifies two broad families of prior work, each with distinct limitations that motivate the synthetic data approach.

Search-Based Approaches with Neural Guidance

The first family consists of methods that use neural models to guide tree search through the space of possible proof steps in an interactive theorem proving environment (Section 2). These include GPT-f (Polu and Sutskever, 2020), Proof Artifact Co-Training (Han et al., 2021), Hypertree Proof Search (Lample et al., 2022), ReProver (Yang et al., 2024), and curriculum learning methods (Polu et al., 2022). In this paradigm, the model operates as a tactic generator: given the current proof state (goals, hypotheses, and the local context), it proposes the next proof step, which is then checked by the proof assistant. The process iterates, with the model receiving the updated proof state, until the proof is complete or a computational budget is exhausted.

The paper acknowledges the achievements of these methods — Hypertree Proof Search, for example, achieves 41.0% on miniF2F-test at 64×5000 search steps with a 600M parameter model (Table 1), and Curriculum Learning reaches 36.6% at 64×8×512 on miniF2F-test. However, the authors identify a fundamental limitation:

"These approaches primarily utilize reinforcement learning techniques to enhance the accuracy of the model... Since the search space is significantly large, the searching process consumes considerable time and computing resources." (Section 2)

The search space for even moderately complex theorems is vast. At each step, the model must choose from hundreds of possible tactics, apply them to potentially many subgoals, and recursively explore branches that may dead-end after many steps. The computational cost of running thousands of interactive search episodes per theorem — with the overhead of communicating between the LLM and the proof assistant at each step — makes these methods computationally expensive to deploy and difficult to scale to harder problems. Moreover, these methods do not address the training data bottleneck: they still require a seed corpus of formal proofs to train the tactic generator, and they do not create new training data as a side effect.

Whole-Proof Generation Methods

The second family bypasses interactive search by having the model generate the complete proof in a single pass (Section 2). This includes Baldur (First et al., 2023), DSP (Jiang et al., 2022b), Subgoal-based Demonstration Learning (Zhao et al., 2023), and LEGO-Prover (Xin et al., 2023). These methods are computationally much cheaper per attempt — there is no back-and-forth with the proof assistant during generation, only a single verification step at the end. However, their performance is limited by a different bottleneck: the quantity and diversity of training data available for fine-tuning.

The paper notes that even the most advanced LLMs, when applied to whole-proof generation without domain-specific fine-tuning, achieve relatively modest results. GPT-4, despite its massive scale and general reasoning capabilities, achieves only 23.0% on miniF2F-test with 64 samples (Table 1). DeepSeekMath-Base 7B, pre-trained specifically on mathematics but not fine-tuned on formal proofs, achieves 27.5% at 128 samples. These numbers are far below what would be needed for practical mathematical assistance, and they highlight that general mathematical reasoning ability — which both GPT-4 and DeepSeekMath possess — does not directly translate into formal proof generation capability without exposure to formal proof data.

Autoformalization: Promising but Under-Scaled

A third line of work, which the paper builds on most directly, is autoformalization — the use of LLMs to translate natural language mathematical statements into formal specifications (Wu et al., 2022; Jiang et al., 2022b; Huang et al., 2024). Autoformalization is attractive because it could, in principle, unlock the vast corpus of informal mathematics (textbooks, competition problems, research papers) as a source of training data for formal provers. However, prior autoformalization efforts have been limited in scale:

"These datasets remain smaller than needed and are limited to small mathematical benchmarks, leading to only minor improvements in training outcomes for language models." (Section 2)

The MMA dataset (Jiang et al., 2023), which the paper uses as a starting point, back-translates mathlib theorems into natural language and then asks a model to re-formalize them — but this is inherently bounded by the size of mathlib itself. Other approaches use rule-based transformations of existing theorems (Wu et al., 2020; Wang and Deng, 2020; Xiong et al., 2023), which are "constrained by their reliance on predefined rules and lack flexibility for broader applications" (Section 2). No prior work had demonstrated autoformalization at the scale needed to meaningfully improve whole-proof generation performance — a gap the paper aims to fill with its 8 million theorem-proof pair dataset.

How This Paper Positions Itself

The paper positions itself at the intersection of three converging trends: the availability of powerful pre-trained mathematical LLMs (specifically DeepSeekMath 7B), the existence of proof assistants with robust verification capabilities (Lean 4), and the recognition that data, not architecture, is the binding constraint. Its contribution is not a new search algorithm or a new model architecture, but rather a data-centric pipeline that bootstraps a neural theorem prover from a small seed of formal proof data (the MMA dataset) to a large-scale synthetic dataset through iterative self-improvement.

This positioning is explicitly contrasted with existing work along several dimensions:

Versus search-based methods. The paper does not compete on search efficiency; instead, it aims to make the underlying model so capable that search becomes less necessary. The whole-proof generation results — 46.3% at 64 samples and 52% cumulatively — demonstrate that with sufficient training data, a model can directly generate valid proofs for nearly half of the miniF2F problems without any interactive search at all, substantially outperforming search-based methods that require thousands of interactive steps per problem (Table 1). This is a fundamentally different scaling philosophy: invest compute in training (through data synthesis) rather than in inference-time search.

Versus prior autoformalization. The paper's key insight is that autoformalization must be done at industrial scale to matter. Moving from datasets of thousands or tens of thousands of examples to 8 million requires solving several engineering and quality-control challenges: how to filter low-quality formalizations at scale, how to handle unprovable statements without wasting compute, and how to iteratively improve the autoformalization model using its own verified outputs. The paper treats these as first-class problems and develops specific mechanisms for each — quality scoring models, hypothesis rejection via negation-proving, and a dual-stream proof search that simultaneously attempts the original statement and its negation to quickly terminate on unprovable statements (Section 3.3).

Versus general-purpose LLMs. The paper implicitly argues that domain-specific data synthesis and fine-tuning is more effective than relying on the general reasoning capabilities of frontier models like GPT-4. The performance gap is stark: DeepSeek-Prover (7B parameters, fine-tuned on synthetic data) achieves roughly double the pass rate of GPT-4 (unknown but vastly larger parameter count) on miniF2F-test with comparable sampling budgets. This supports the thesis that formal theorem proving is a skill that can be taught through specialized training data, and that models explicitly trained for this task can punch well above their weight class relative to general-purpose systems.

The iterative self-improvement framing. The paper draws on the expert iteration paradigm (Polu and Sutskever, 2020) but applies it at an unprecedented scale and with a novel mechanism: rather than iterating on proof search within a fixed set of theorems, the paper iterates on the entire pipeline — autoformalization, proof generation, and model fine-tuning — with each cycle producing a stronger model that generates higher-quality data for the next cycle. This creates a virtuous cycle where better models produce better data, and better data produces better models (Section 3.4). The ablation in Table 4 confirms this: pass rates on miniF2F improve from 32.3% to 42.0% to 50.0% (at pass@128) across three successive training iterations, demonstrating that the gains compound.

The Specific Gap: Bridging Informal and Formal Mathematics at Scale

The paper's core technical gap can be stated precisely: there exists a large corpus of informal mathematical problems (869,659 competition problems at the high-school and undergraduate level) and a small corpus of formal mathematical proofs (mathlib, containing perhaps tens of thousands of theorems), with no scalable, automated bridge between them. The paper's approach — autoformalization with quality control, parallel proof search with negation-based early termination, and iterative model refinement — is designed to construct exactly this bridge. The target domain (algebra and number theory at competition levels) is chosen strategically: these problems have well-defined formalizations and solutions that exercise non-trivial reasoning, but do not require the deep theoretical machinery (e.g., algebraic geometry, advanced topology) that would make autoformalization infeasible with current models (Section 3.1).

The scale of the resulting dataset — 8 million theorem-proof pairs after filtering and iterative refinement — represents a roughly two to three order of magnitude increase over previously available formal proof datasets. This quantitative leap is what enables the qualitative leap in model performance, establishing the paper's central claim that data scale, achieved through systematic synthetic data generation, is the key to advancing neural theorem proving.

3. Technical Approach

3.1 Reader orientation (approachable technical breakdown)

The paper builds a data generation pipeline — not a new model architecture or a new search algorithm, but a system for automatically producing millions of verified formal proof examples from a large collection of informal math problems. The system solves the chicken-and-egg problem of neural theorem proving: you need a good model to generate formal proofs, but you need formal proofs to train a good model. The "shape" of the solution is an iterative self-improvement loop: start with a weak model, use it to autoformalize informal problems into formal statements and generate proofs, verify those proofs with Lean 4 to keep only correct ones, fine-tune the model on the verified data to make it stronger, then repeat the cycle with the improved model — each iteration producing higher-quality data and a stronger prover.

3.2 Big-picture architecture (diagram in words)

The system (Figure 1) has five interconnected components arranged in a cycle:

1. Informal Problem Corpus — a curated dataset of 869,659 natural language math problems (high-school and undergraduate competition problems, primarily algebra and number theory), scraped from online resources and cleaned. This is the raw input.

2. Autoformalization Module — takes an LLM (initialized from DeepSeekMath-Base 7B, fine-tuned on back-translated mathlib data) and prompts it to translate each natural language problem into a formal Lean 4 statement. Output: candidate formal statements with varying quality.

3. Quality Filtering Module — two-stage filter that (a) scores each formal statement on a 5-point quality scale ("excellent" through "poor") using the model itself with a chain-of-thought rubric, discarding "fair" and "poor" statements, and (b) applies hypothesis rejection: the model attempts to prove the negated statement (or the statement with False as the conclusion) — success means the hypotheses are inconsistent, and the statement is discarded. Output: 712,073 high-quality formal statements.

4. Proof Generation and Verification Module — takes each filtered formal statement and runs dual concurrent proof searches: one thread attempts to prove the statement $\Gamma \vdash P$, the other attempts to prove its negation $\Gamma \vdash \neg P$. Each thread samples up to $k$ proofs from the model. The Lean 4 verifier checks each candidate. The search terminates as soon as either thread succeeds — if the negation is proved, the original statement is known to be unprovable (or incorrectly formalized) and is discarded. Output: validated theorem-proof pairs (either $P$ with proof, or $\neg P$ with proof — both serve as training data).

5. Iterative Fine-Tuning Loop — the validated theorem-proof pairs are aggregated and used to fine-tune the model. The strengthened model then replaces the previous one in the autoformalization module, and the entire pipeline repeats. The cycle continues until marginal improvements are observed (three iterations in practice). Output: the final DeepSeek-Prover model plus the 8 million theorem-proof synthetic dataset.

3.3 Roadmap for the deep dive

• First, the autoformalization step — how the model converts natural language to Lean 4 statements, what seed training data enables this, and what prompts are used — because autoformalization is the bridge that connects the informal corpus to the formal pipeline.

• Second, the quality filtering mechanisms — the model-based scoring rubric and the hypothesis rejection strategy — because these determine which autoformalized statements survive to be proved, and understanding the failure modes they address (overly simple statements, inconsistent hypotheses) is essential to understanding why naive autoformalization at scale fails.

• Third, the dual-stream proof search with negation-based termination — the core efficiency innovation that prevents wasting compute on unprovable statements — because this is what makes large-scale proof generation computationally feasible when a significant fraction of autoformalized statements are incorrect.

• Fourth, the iterative enhancement cycle — how the model is fine-tuned on validated data and fed back into the pipeline — because this is the engine that compounds gains across iterations and produces the final dataset of 8 million examples.

• Fifth, training configuration and inference details for DeepSeek-Prover — the concrete hyperparameters, model initialization, and generation settings — because these are the engineering choices that make the pipeline reproducible.

3.4 Detailed, sentence-based technical breakdown

This is primarily a data-centric systems paper whose core idea is that a neural theorem prover can be bootstrapped from a small seed of formal proof data through large-scale autoformalization of informal mathematics, quality-controlled by verifier feedback, and iteratively refined such that the model's own verified outputs become the training data for its next version — creating a self-reinforcing cycle where model capability and data quality co-evolve.

Autoformalization: Translating Natural Language to Lean 4 Statements

The autoformalization module converts informal mathematical problems — written in English with standard mathematical notation — into formal Lean 4 statement declarations. This is the critical bridge because the raw training data for the prover must be formal statements paired with formal proofs, but the available informal corpus (869,659 problems) contains only natural language descriptions.

Seed training for autoformalization. The initial model (DeepSeekMath-Base 7B, a decoder-only transformer pre-trained on 120 billion math-related tokens) cannot autoformalize out of the box — it has never seen paired informal-formal data. To bootstrap this capability, the authors fine-tune it on the MMA dataset (Jiang et al., 2023), which contains formal statements from Lean 4's mathlib (at a specific commit: 64528268b3c2cf578639bc479828882a9ecd3a82) that were back-translated into natural language by GPT-4. The back-translation process works as follows: take each formal theorem statement in mathlib, ask GPT-4 to describe it in natural language, producing a synthetic informal description. This creates a parallel corpus of (natural language problem description, formal Lean 4 statement) pairs. Fine-tuning DeepSeekMath-Base 7B on this corpus teaches the model to map informal descriptions to formal syntax.

Why this approach rather than directly using mathlib statements without back-translation? Because the model needs to learn the mapping from informal to formal — if it only sees formal statements during fine-tuning, it cannot generalize to converting new informal problems. The back-translation creates a supervised translation task where the input is natural language and the output is Lean 4 code, which is exactly the capability needed for autoformalization.

Autoformalization prompt structure. The fine-tuned model is then applied to the 869,659 informal competition problems. The prompt follows a simple template (Section 3.1):

Mathematical Problem in Natural Language:
{$informal_statement_with_answers}

Translate the problem to Lean 4 (only the core declaration):
```lean4

The model responds with a Lean 4 declaration — typically an example or theorem statement that captures the mathematical claim. For instance, the informal problem "Prove that the determinant of a specific 3×3 matrix of cosines is zero" becomes (Section 5.1):

example (a b : ℝ) :
    Matrix.det ![![1, Real.cos (a - b), Real.cos a],
                  ![Real.cos (a - b), 1, Real.cos b],
                  ![Real.cos a, Real.cos b, 1]] = 0

The model must recognize that cos maps to Real.cos, that a - b is subtraction in ℝ, and that the matrix determinant is Matrix.det applied to a ![] list-of-lists representation — all without explicit guidance in the prompt, relying entirely on the mapping learned during fine-tuning.

Scope limitation. The authors deliberately restrict autoformalization to high-school and undergraduate competition problems with a focus on algebra and number theory (and to a lesser extent combinatorics, geometry, and statistics). Problems with "explicit conditions and well-defined goals are typically easier to formalize compared to advanced mathematical topics that necessitate intricate definitions and constructions" (Section 3.1). This is a practical engineering choice: autoformalization of, say, sheaf cohomology would require the model to generate correct definitions of sheaves, abelian categories, and derived functors — far beyond what current LLMs can reliably produce. By staying within self-contained competition problems, the autoformalization task reduces to translating relatively bounded mathematical concepts (equations, inequalities, divisibility, trigonometric identities) into their mathlib equivalents.

Scale of autoformalization. After quality filtering (described next), the pipeline produces 712,073 formal statements from the initial 869,659 informal problems — a yield of approximately 82%. The 18% loss comes from statements that fail the quality filter or the hypothesis rejection test.

Quality Filtering: Scoring and Hypothesis Rejection

Autoformalized statements suffer from two distinct problems that require separate filtering mechanisms. The first is triviality — the model may produce formal statements that are technically correct but mathematically uninteresting (e.g., 2 + 2 = 4). The second is logical inconsistency — the model may produce statements with contradictory hypotheses that make the conclusion vacuously true but mathematically meaningless. The quality filtering module (Section 3.2) addresses both.

Model-Based Quality Scoring

The authors train the model to evaluate the quality of its own autoformalized statements using a detailed rubric. The prompt (full text in Appendix A.1) instructs the model to assess each statement across five criteria using chain-of-thought reasoning:

1. Relevance to Current Research — does the statement address an actively researched problem or concept?
2. Complexity and Depth — is the statement challenging enough to exercise non-trivial reasoning?
3. Interdisciplinary Potential — does the statement connect mathematics with other fields?
4. Community Needs and Gaps — does it fill an identified need in the formal mathematics community?
5. Innovativeness — does it propose new methods, concepts, or applications?

The model is provided with few-shot examples from miniF2F-valid (the validation split of the miniF2F benchmark, which contains high-quality competition problems) as exemplars of what constitutes a good formal statement. For each candidate statement, the model produces a structured response containing: a natural language explanation of what the statement says, a line-by-line analysis against each criterion, and a final categorical rating from the set {excellent, good, above average, fair, poor}.

Statements rated fair or poor are discarded. The paper reports that "manual review of these scores confirmed that the model's evaluations closely matched human intuition and expectations" (Section 3.2), though no quantitative inter-rater agreement metric is provided.

Why this five-criteria rubric rather than a simpler approach like filtering by proof length or statement length? Because mathematical depth is not purely a function of syntactic complexity. A short statement about a subtle inequality may be far more valuable as training data than a long but mechanical algebraic manipulation. The rubric attempts to capture the semantic quality of the formalization — whether it represents a genuine mathematical problem worth solving. The chain-of-thought requirement forces the model to articulate its reasoning before assigning a rating, which the authors find improves reliability compared to directly outputting a score.

Ablation evidence. The effectiveness of this filtering is demonstrated in Table 3: models trained on high-score proof data outperform models trained on low-score proof data by 4.5 percentage points on miniF2F pass@128 (specifically, the high-score model achieves a certain pass rate, and the low-score model achieves 4.5% lower). The magnitude of this gap validates that the scoring model meaningfully separates high-quality from low-quality formalizations.

Hypothesis Rejection via Negation-Proving

The second filtering mechanism addresses a more subtle problem: formal statements with inconsistent hypotheses. Consider the example from Section 3.2:

example (θ : ℝ) (h₀ : ∀ z : ℂ, z^2 = -1 ∧ z^3 = -1 ∧ z^6 = 1)
  (h₁ : Real.tan θ = 2 * Real.sqrt 3) : θ = 5 * Real.pi / 3

The hypothesis h₀ asserts that every complex number $z$ simultaneously satisfies $z^2 = -1$, $z^3 = -1$, and $z^6 = 1$. This is mathematically impossible — no single complex number satisfies all three equations simultaneously, let alone every complex number. Since False implies anything in classical logic, this statement is vacuously provable: you could "prove" the conclusion $\theta = 5\pi/3$ by simply deriving a contradiction from h₀ and then applying the principle of explosion (ex falso quodlibet). However, such a proof teaches the model nothing useful — the reasoning that the hypotheses are contradictory says nothing about whether the relationship between $\theta$ and the tangent condition actually holds.

To eliminate these vacuous statements, the authors implement hypothesis rejection: for each autoformalized statement, the model attempts to prove a modified version where the conclusion is replaced by False:

example (θ : ℝ) (h₀ : ∀ z : ℂ, z^2 = -1 ∧ z^3 = -1 ∧ z^6 = 1)
  (h₁ : Real.tan θ = 2 * Real.sqrt 3) : False := by
  simpa using h₀ 1

If the model succeeds in proving False (by instantiating the universal quantifier ∀ z : ℂ with 1 and deriving a contradiction from the resulting equations), then the original hypotheses are inconsistent, and the statement is discarded regardless of its quality score. The key insight: proving False from the hypotheses is typically much easier than proving the original conclusion because any contradiction will do — the model only needs to find one counterexample to the universal claim. In the example above, substituting $z = 1$ yields $1 = -1$, which is immediately false.

This mechanism serves a dual purpose. First, it acts as a filter. Second, the proofs of False themselves become training data — they teach the model to recognize and exploit inconsistent hypotheses, which is a useful skill for theorem proving in general (e.g., case analysis where some branches are vacuous).

Operational details. The hypothesis rejection is integrated into the proof search phase: for each statement, the model attempts to prove both the original statement and the False variant. If the False variant succeeds first, the statement is discarded and the proof of False is saved as training data. If the original succeeds first, the statement-proof pair is kept. If neither succeeds within the budget, the statement is also discarded (it may be true but too hard, or false but too hard to prove false).

Dual-Stream Proof Search with Negation-Based Early Termination

Once filtered formal statements are obtained, the pipeline must generate proofs for them. However, a significant fraction of autoformalized statements — the paper estimates at least 20% even after quality filtering — are incorrectly formalized, meaning they do not correspond to true mathematical statements in Lean 4's logic. Applying standard brute-force proof search to these statements wastes enormous compute: the model repeatedly attempts to prove an unprovable statement until a time limit or attempt budget is exhausted, generating no useful training data.

The core efficiency innovation (Section 3.3) exploits the logical symmetry between a statement and its negation to parallelize the proof search and terminate early when a statement is detected as false.

The dual-stream architecture. For each formal statement $\Gamma \vdash P$ (where $\Gamma$ represents the hypotheses and context, and $P$ is the conclusion), the system launches two independent proof search streams:

• Stream 1 attempts to prove $\Gamma \vdash P$ (the original statement).
• Stream 2 attempts to prove $\Gamma \vdash \neg P$ (the negation of the statement).

Each stream samples up to $k$ complete proof candidates from the model (where $k$ is a hyperparameter controlling the generation budget per stream). Each candidate is verified by Lean 4. The search terminates as soon as either stream produces a valid proof:

• If Stream 1 succeeds first, the theorem $P$ is true (relative to the hypotheses $\Gamma$), and the pair $(P, \text{proof})$ is saved as training data.

• If Stream 2 succeeds first, the theorem $\neg P$ is true, meaning $P$ is false. The original statement is discarded (it was incorrectly formalized), but the pair $(\neg P, \text{proof})$ is saved as training data — proving negations of false statements is itself a useful theorem-proving skill.

• If neither stream succeeds within $k$ attempts, the statement is discarded. It may be true but beyond the model's current capability, or false but too hard to disprove.

Why this doubles as data augmentation. The paper frames the dual-stream approach as "a form of data augmentation" (Section 3.3) because both successful outcomes contribute to the training corpus. If the original formalization was correct, the model learns to prove the intended theorem. If the original formalization was incorrect, the model still learns something valuable: how to construct a counterexample or derive a contradiction from an impossible set of hypotheses. In both cases, the generated proof is verified correct by Lean 4, so there is no risk of contaminating the training data with incorrect reasoning.

Comparison to single-stream search. In a conventional single-stream setup, the model would attempt to prove $P$ repeatedly until success or budget exhaustion. If $P$ is false, all $k$ attempts fail, wasting the entire compute budget with no training data produced. In the dual-stream setup, a false $P$ is detected when Stream 2 succeeds — potentially much faster than exhausting $k$ attempts — and the proof of $\neg P$ becomes usable training data. The paper does not report exact speedup factors, but the logic is straightforward: the expected time to termination is the minimum of the time to prove $P$ and the time to prove $\neg P$, which is strictly less than or equal to the time to prove $P$ alone (assuming the negation is sometimes easier to prove than the original).

Integration with hypothesis rejection. The dual-stream approach subsumes the hypothesis rejection mechanism described earlier: proving $\neg P$ from inconsistent hypotheses is equivalent to proving $\Gamma, P \vdash \text{False}$, which is what hypothesis rejection does. The dual-stream formulation is more general because it handles cases where the hypotheses are consistent but $P$ is still false (e.g., a formalization that incorrectly asserts "all primes are odd" would be disproved by finding a counterexample, $2$, without the hypotheses themselves being contradictory).

Budget allocation. The paper sweeps $k$, the number of attempts per stream, but does not specify a fixed value used in the final pipeline. In the evaluation (Table 1), generation budgets range from greedy (1 attempt) to 65,536 attempts, with the model's pass rate improving from 30.0% (greedy) to 50.0% (65,536 attempts) on miniF2F-test. The budget for synthetic data generation is presumably chosen to balance throughput (more attempts = more proofs found but slower per statement) against coverage (fewer attempts = faster but misses provable statements).

Iterative Enhancement: Fine-Tuning and Pipeline Recycling

The iterative enhancement loop (Section 3.4) is the mechanism that transforms a moderately capable autoformalizer into a strong theorem prover. The core insight: the model's autoformalization and proof-generation capabilities are bottlenecked by its training data, but its own verified outputs — once filtered through Lean 4 — become high-quality training data for the next iteration.

The cycle in detail. Each iteration $i$ proceeds as follows:

1. Autoformalization: Model $M_i$ (initialized from DeepSeekMath-Base 7B or the previous iteration's checkpoint) translates the 869,659 informal problems into formal Lean 4 statements.

2. Quality filtering: Model-based scoring and hypothesis rejection are applied to the autoformalized statements, yielding a curated set $\mathcal{S}_i$ of (relatively) high-quality formal statements.

3. Proof generation: Model $M_i$ attempts to generate proofs for statements in $\mathcal{S}_i$ using the dual-stream search. Validated proofs (whether of the original statement or its negation) are collected into a dataset $\mathcal{D}_i$.

4. Fine-tuning: Model $M_i$ is fine-tuned on $\mathcal{D}_i$ (combined with data from all previous iterations: $\mathcal{D}_1 \cup \mathcal{D}_2 \cup \dots \cup \mathcal{D}_i$) using supervised learning on the correct proof tokens, producing Model $M_{i+1}$.

5. Termination check: If $M_{i+1}$ shows marginal or no improvement over $M_i$ on a held-out validation task (presumably miniF2F-valid), the cycle stops. Otherwise, $i \leftarrow i+1$ and return to step 1.

Why iterative fine-tuning compounds. The effectiveness of the second iteration depends critically on the quality of the data produced in the first iteration. If Model $M_1$ (fine-tuned only on the MMA dataset) generates low-quality autoformalizations and few correct proofs, then $\mathcal{D}_1$ may be too small or too noisy to meaningfully improve the model. The paper's results suggest this is not the case: even $M_1$ produces enough correct proofs to bootstrap the cycle. This is partly because the MMA dataset provides a reasonable starting point for autoformalization (it covers a broad range of mathlib theorems), and partly because the quality filtering and dual-stream search salvage useful data even from imperfect formalizations (negation proofs, hypothesis rejection proofs).

Scaling behavior across iterations. Table 4 quantifies the improvement:

The jump from iteration 1 to 2 (+9.7 percentage points) is larger than from iteration 2 to 3 (+8.0 percentage points), suggesting diminishing returns — which is expected as the model asymptotically approaches the quality ceiling imposed by the informal problem corpus and the inherent difficulty of the benchmark. The paper reports that the process "continues until no further gains are observed" (Section 3.4), implying they ran at least three iterations and potentially more but observed marginal improvements after the third.

Data accumulation. The final dataset comprises 8 million theorem-proof pairs, aggregated across all iterations. The paper does not break down the contribution per iteration, but the cumulative nature of the training data — each iteration fine-tunes on all previous data plus new data — means the model is exposed to an increasingly diverse set of formal statements and proof strategies.

Fine-tuning configuration details. For each iteration, the model is fine-tuned using:

• Global batch size: 512
• Constant learning rate: $1 \times 10^{-4}$
• Warmup steps: 6,000
• Optimizer: not explicitly stated, but inherited from DeepSeekMath-Base training (presumably AdamW, given the use of warmup)
• Base model: DeepSeekMath-Base 7B, a decoder-only transformer pre-trained on 120 billion math-related tokens (Shao et al., 2024)

The use of a constant learning rate with warmup is standard in LLM fine-tuning and suggests the authors prioritize simplicity over extensively tuned schedules. The global batch size of 512 is relatively large for a 7B model, indicating they have sufficient hardware to process many examples in parallel.

Training Data Construction: From Verified Proofs to Fine-Tuning Examples

Once a proof is verified by Lean 4, it becomes a supervised training example. The training objective is standard autoregressive language modeling on the proof tokens, conditioned on the formal statement. That is, given a formal statement $S$ (the example or theorem declaration including hypotheses and conclusion), the model is trained to maximize:

$P(\text{proof} \mid S) = \prod_{t=1}^{T} P(\text{token}_t \mid S, \text{token}_{<t})$

where $T$ is the length of the proof in tokens and $\text{token}_{<t}$ represents the prefix of the proof up to position $t-1$.

What this computes: The standard next-token prediction loss for language models, applied specifically to the proof body given the formal statement as context. The model sees the formal statement, then must generate the proof tokens autoregressively. The loss is computed only on the proof tokens (the statement tokens are part of the context but not predicted).

Why this form: This is the standard fine-tuning objective for sequence-to-sequence tasks in decoder-only models. It directly trains the model to generate proofs from statements, which is exactly the capability needed at inference time. An alternative would be to train on pairs of (proof state, next tactic) as in interactive theorem proving, but that would require the interactive overhead during data generation and would produce step-by-step rather than whole-proof training data — the paper deliberately chooses whole-proof generation to avoid this overhead.

What data gets included. The training corpus includes:

1. Proved original statements: (statement, proof) pairs where Stream 1 succeeded, meaning the autoformalized statement was mathematically correct and provable.

2. Proved negations: (negation_statement, proof) pairs where Stream 2 succeeded, meaning the original statement was false. These examples teach the model to recognize false statements and provide counterexamples.

3. Hypothesis rejection proofs: (statement_with_False_conclusion, proof) pairs from the quality filtering stage, where the model derived False from inconsistent hypotheses. These teach the model to detect and exploit logical contradictions.

The common thread: every training example is verified correct by Lean 4 before inclusion. This eliminates the possibility of training on hallucinated or incorrect proofs, which is a critical distinction from naive self-training approaches where a model might reinforce its own errors.

Data diversity. Because the informal problem corpus spans multiple mathematical domains (algebra, number theory, combinatorics, geometry, statistics at high-school and undergraduate competition levels), the resulting formal statements and proofs cover a correspondingly diverse range of mathematical concepts and proof techniques. The paper notes that problems "often involve complex solution techniques, making them excellent candidates for constructing proof data to improve theorem-proving capabilities" (Section 3.1). This diversity is important for generalization: a model trained only on, say, algebraic identities would not learn induction or case analysis, which are essential for broader theorem proving.

Verification environment. All proof verification is performed using Lean 4, specifically version v4.7.0-rc2 (as noted in the footnote: leanprover/lean4:v4.7.0-rc2). The verification is done within a Docker container or equivalent environment, with a preamble that imports the necessary mathlib modules (listed in Appendix A.4). The preamble includes imports for algebra, analysis, combinatorics, data structures, number theory, and topology — ensuring that the vast majority of mathlib is available during verification. The maxHeartbeats option is set to 0 (disabling the heartbeat limit), and trace.aesop options are enabled for debugging.

Inference: Whole-Proof Generation with Sampling

At inference time, DeepSeek-Prover generates proofs using whole-proof generation — the model produces the complete proof text in one forward pass, without iterative interaction with Lean 4. This is in contrast to step-by-step methods like GPT-f or ReProver, which generate one tactic at a time and query the proof assistant after each step.

Why whole-proof generation over interactive search. The paper's rationale is efficiency: whole-proof generation "bypasses the iterative interaction during proof generation" (Section 2), reducing wall-clock time and computational overhead. The trade-off is that the model cannot recover from errors mid-proof — if it makes a mistake on step 3 of a 10-step proof, the entire proof fails verification, and a new sample must be generated from scratch. The model's high single-sample accuracy (30.0% greedy, 50.0% at 65,536 samples on miniF2F-test) is what makes this viable: with a 30% chance of generating a correct proof on the first try, the expected number of samples to find a proof for a given problem is roughly $1 / 0.30 \approx 3.3$, which is acceptable.

Sampling strategy. The evaluation uses pass@k: for each problem, the model generates $k$ independent proof candidates (with temperature sampling, though the specific temperature is not stated in the main paper), each verified by Lean 4. The problem is considered solved if at least one candidate passes verification. The cumulative pass rate is computed across all $k$ samples. The paper reports results at multiple values of $k$: greedy (1 sample), 64, 128, 8192, and 65536 samples, as well as a cumulative metric that aggregates across all samples generated (i.e., what fraction of problems are solved by any sample, regardless of $k$).

Performance scaling with sample count. On miniF2F-test (Table 1):

• Greedy (1 sample): 30.0%
• 64 samples: 46.3%
• 128 samples: 46.3% (plateau)
• 8,192 samples: 48.8%
• 65,536 samples: 50.0%
• Cumulative: 52.0%

The diminishing returns at higher sample counts are expected: problems that the model can solve are typically solved within the first few samples, while problems the model fundamentally cannot handle (e.g., those requiring concepts outside its training distribution) remain unsolved regardless of sample count. The jump from greedy to 64 samples (+16.3 percentage points) represents problems where the model's correct proof is in its distribution but not its mode — the model knows how to prove these but needs multiple attempts to sample a correct trajectory. The plateau from 64 to 128 (0.0 improvement) suggests that by 64 samples, the model has largely exhausted the set of problems it can solve via random sampling of its output distribution. The further improvements at 8,192 and 65,536 (+2.5 and +1.2 points, respectively) represent the thin tail of problems where correct proofs are rare events in the sampling distribution.

Design Choices and Their Justifications (Summary)

• Autoformalization via back-translated mathlib over directly using mathlib statements: creates a supervised translation task (informal → formal) that teaches the model the mapping it needs for autoformalization, rather than just exposing it to formal syntax.

• Domain restriction to competition-level algebra and number theory over attempting all of mathematics: autoformalization of advanced topics (topology, algebraic geometry) would require generating correct definitions of deep mathematical structures, which current LLMs cannot reliably do. Competition problems have self-contained, well-defined formalizations that exercise non-trivial reasoning.

• Model-based quality scoring with chain-of-thought over rule-based filters (e.g., statement length, number of hypotheses): mathematical quality is semantic, not syntactic. The rubric and chain-of-thought prompt forces the model to articulate why a statement is interesting, producing more reliable filtering than surface-level heuristics.

• Hypothesis rejection via False-conclusion proving over directly checking satisfiability of hypotheses (which is undecidable in general): proving False from inconsistent hypotheses is often easy (a single counterexample suffices), whereas proving satisfiability may require constructing a model — a much harder task. The False-proving approach leverages the theorem prover's existing capability rather than requiring a separate satisfiability solver.

• Dual-stream proof search over single-stream brute force: exploits the logical symmetry between $P$ and $\neg P$ to early-terminate on false statements, converting wasted compute (failed attempts on unprovable statements) into productive compute (proving negations, which become training data). This is critical for scaling to 8 million examples given that at least 20% of autoformalized statements are incorrect.

• Whole-proof generation over interactive step-by-step search: trades off error recovery for simplicity and throughput. The model generates one complete proof per forward pass; verification is a single Lean 4 check at the end. This eliminates the overhead of maintaining proof state, communicating between model and verifier at each step, and handling backtracking — all of which are necessary in interactive search.

• Iterative fine-tuning with cumulative data over single-pass training: each iteration's model is stronger, producing higher-quality autoformalizations and more proofs, which in turn creates better training data for the next iteration. The compounding effect (32.3% → 42.0% → 50.0%) demonstrates that the data quality improvement from iteration to iteration is real and significant.

• Use of DeepSeekMath-Base 7B over a general-purpose LLM: the model's pre-training on 120 billion math-specific tokens provides a strong inductive bias for mathematical reasoning. Fine-tuning on formal proof data then specializes this general mathematical capability to the specific syntax and proof strategies of Lean 4. A general-purpose model would need to learn both mathematical reasoning and formal syntax from scratch, requiring far more formal proof data than is available even with synthetic generation.

4. Key Insights and Innovations

Innovation 1: Autoformalization as a Data Generation Engine, Not a Translation Task

The paper's most fundamental conceptual move is to reframe autoformalization from a translation accuracy problem into a data generation throughput problem. Prior autoformalization work (Wu et al., 2022; Jiang et al., 2022b; Huang et al., 2024) treated the task as faithful semantic translation: take a carefully curated benchmark statement, produce an equivalent formal statement, and evaluate whether the formalization is correct. This framing implicitly assumes correctness is the binding constraint — that what limits neural theorem provers is the precision of their autoformalization, and that better translation quality yields better training data.

This paper inverts that assumption. The key diagnostic move is recognizing that imperfect autoformalization is not a failure mode to be eliminated but a feature to be exploited. When the model produces an incorrectly formalized statement — one that is mathematically false in Lean 4's logic — the dual-stream proof search does not simply discard it as waste. Instead, the system proves its negation, generating a verified proof that the statement is false. This proof-of-falsity becomes training data that teaches the model to recognize and refute incorrect formalizations in future iterations. The insight is that a pipeline that generates 8 million theorem-proof pairs at 80% correctness is more valuable than one that generates 100,000 pairs at 99% correctness, because the downstream prover benefits from both true proofs (which teach constructive reasoning) and false refutations (which teach logical discrimination and hypothesis checking). This is a fundamental shift from "autoformalization quality → model quality" to "autoformalization quantity, with verification feedback → model quality," and it repositions the entire enterprise from a natural language processing problem to a reinforcement learning-style data generation problem.

The significance extends beyond raw performance. This framing resolves a tension that had been implicit in prior work: autoformalization was always going to be noisy at scale because informal mathematical language is ambiguous, and the model cannot distinguish a missing condition from a deliberately general statement. The standard response was to invest in better translation models. This paper's response is to build a system that thrives on the noise — converting failed formalizations into valuable training signal through the symmetry of logical negation. Conceptually, this is analogous to how contrastive learning methods use negative examples to sharpen representations, but applied at the level of logical proof generation rather than embedding space.

The evidence anchoring this claim appears in Section 3.3 and the ablation in Table 2: models trained with autoformalized data substantially outperform those trained solely on human-authored mathlib theorems, even though a non-trivial fraction of the autoformalized statements are incorrect (the paper estimates at least 20%). If correctness were the binding constraint, this would be impossible — noisy data should degrade, not improve, performance. The fact that it improves demonstrates that the training signal from correct proofs in the synthetic dataset outweighs any noise from incorrectly formalized statements that slipped through filtering, and that the rejected incorrect statements (those caught by negation-proving and hypothesis rejection) still contributed training data of a different kind.

Innovation 2: The "Proof of Negation as Data Augmentation" Principle

A closely related but distinct conceptual contribution is the principle that proving the negation of a false formal statement is as valuable for training as proving a true statement — and that a system can be designed to treat these outcomes symmetrically. This is not an obvious design choice. The dominant assumption in theorem-proving data construction, from mathlib curation to prior synthetic data efforts, has been that training examples should consist of true theorems with valid proofs. False statements are typically seen as failures of the formalization process to be filtered and discarded.

The paper argues — implicitly, through its pipeline design — that this assumption is wrong for neural theorem provers. Proving that a statement is false requires a specific kind of reasoning: constructing a counterexample, deriving a contradiction from the hypotheses, or showing that the conclusion violates some known invariant. These are genuine mathematical skills that a competent theorem prover must possess, and they are underrepresented in datasets built from human-authored formal mathematics (where mathematicians rarely bother to formalize "this statement is false" unless the falsehood itself is mathematically interesting). By systematically generating proofs of negated autoformalized statements, the synthetic data pipeline produces training examples that teach the model a capability — refutation and counterexample construction — that is essential for interactive theorem proving (where users may state conjectures that turn out false) but scarce in existing formal corpora.

This is a new diagnostic concept rather than a metric gain: the paper identifies a class of training data (refutation proofs) that prior work had overlooked and shows how to generate it at scale. The mechanism enabling this — the dual-stream search architecture — is an engineering solution, but the underlying insight is a reconceptualization of what constitutes useful training data for a theorem prover. It's the difference between teaching a student only to prove things that are true and teaching them to also recognize and refute things that are false. The latter is arguably more important for practical theorem proving, where most conjectures turn out to be wrong.

The evidence in Section 3.3 and the case study in Section 5.2 supports this: the model successfully identifies inconsistent hypotheses and provides counterexamples, demonstrating that the refutation training data translates to a real capability. The paper does not isolate the contribution of negation proofs through a dedicated ablation (e.g., training with vs. without refutation examples), which is a limitation, but the principle is conceptually distinct from the autoformalization-as-throughput insight and stands on its own as a contribution to how the field should think about constructing training data for neural provers.

Innovation 3: Iterative Self-Improvement Through Co-Evolution of Formalization and Proof Generation

The paper's third conceptual innovation is the demonstration that autoformalization quality and proof-generation capability co-evolve through iterative fine-tuning on verified outputs, and that this co-evolution can be bootstrapped from a surprisingly small seed dataset. This is not the first application of expert iteration to theorem proving — Polu and Sutskever (2020) introduced the paradigm — but prior applications iterated on proof search within a fixed set of formal theorems. The model would attempt to prove theorems from a static corpus, successful proofs would be added to the training set, and the cycle would repeat with the same theorems. The formal statements themselves never changed; only the proofs did.

What makes this paper's iteration distinctive is that the formal statements evolve alongside the proofs. In iteration 1, a weak autoformalizer (fine-tuned only on the MMA dataset of back-translated mathlib statements) produces noisy formalizations of the 869,659 informal problems. The proofs generated for these formalizations are correspondingly limited in quality. In iteration 2, the model — now fine-tuned on the verified proofs from iteration 1 — produces better autoformalizations of the same informal problems, because it has internalized patterns of correct formal syntax and common pitfalls (e.g., inconsistent hypotheses, missing type constraints) through exposure to both successful proofs and negation refutations. These improved formalizations in turn yield higher-quality proofs, which further train the model.

This creates a virtuous cycle across two distinct capabilities — formalization and proof generation — that are typically treated as separate problems. The conceptual move is recognizing that these capabilities are mutually reinforcing rather than independent: a model that is better at proving theorems is also better at autoformalizing, because generating a correct formal statement requires the same kind of syntactic and semantic understanding as generating a correct proof. The evidence in Table 4 bears this out: pass@128 on miniF2F improves from 32.3% to 42.0% to 50.0% across three iterations, and each iteration uses the same base model architecture and the same informal problem corpus — the only difference is the quality of the synthetic training data, which improved because the model doing the autoformalization and proof generation improved.

This is a fundamental (not incremental) insight because it changes the scaling strategy for neural theorem proving. If autoformalization and proof generation are independent, then improving each requires separate investments: better translation models for formalization, better search algorithms for proof generation. If they co-evolve, then a single investment — in a pipeline that generates verified theorem-proof pairs at scale — improves both simultaneously, with compounding returns. The paper's 4× improvement over GPT-4 on miniF2F while using a 7B-parameter model (vs. GPT-4's estimated hundreds of billions) is the concrete manifestation of this compounding effect.

Innovation 4: Hypothesis Rejection as a Lightweight Logical Sanity Check

A smaller but nonetheless distinctive contribution is the introduction of hypothesis rejection — proving False from a formal statement's hypotheses to detect inconsistent formalizations — as a lightweight, model-based filtering mechanism. Prior work on quality filtering for synthetic formal data relied on either rule-based heuristics (statement length, number of hypotheses, syntactic complexity) or human evaluation, both of which have clear limitations: heuristics cannot detect semantic problems like contradictory hypotheses, and human evaluation does not scale to millions of examples.

The hypothesis rejection approach is elegant because it uses the very capability being trained (theorem proving) to filter the training data for that capability. The model attempts to prove False from the statement's hypotheses, which is typically much easier than proving the original conclusion if the hypotheses are indeed inconsistent — a single counterexample to a universal quantifier suffices, as shown in Section 3.2's example where substituting z = 1 into ∀ z : ℂ, z^2 = -1 ∧ z^3 = -1 ∧ z^6 = 1 immediately yields a contradiction. If the model succeeds, the statement is flagged as having inconsistent hypotheses and discarded. If it fails, the hypotheses are either consistent or the inconsistency is too subtle for the current model to detect — either way, the statement proceeds to proof generation.

This is a diagnostic concept more than a performance gain. It identifies a specific failure mode of autoformalization — the generation of formally valid but mathematically vacuous statements — and provides a principled, scalable method for detecting it. The principle generalizes beyond the specific implementation: whenever a system generates training data through a noisy transformation (autoformalization, back-translation, paraphrasing), a lightweight consistency check that leverages the system's own capabilities can serve as an effective quality filter, provided the check is computationally cheaper than the full task. In this case, proving False from inconsistent hypotheses is cheaper than proving the full theorem because it can succeed on the first counterexample rather than requiring a complete constructive proof.

The evidence supporting this innovation is embedded in the case study of Section 5.2, where the model successfully detects inconsistent hypotheses in an autoformalized statement about matrix determinants and provides a counterexample. The paper does not report what fraction of the 18% of statements filtered out (the difference between the 869,659 input problems and the 712,073 surviving statements) were removed by hypothesis rejection versus quality scoring, which limits the ability to quantify this mechanism's independent contribution. Nevertheless, the principle itself — using the prover to sanity-check its own training data — is a conceptual contribution that could influence data generation pipelines in other formal reasoning domains.

Innovation 5: Whole-Proof Generation as a Contender to Interactive Search at Scale

The paper's final conceptual contribution is an empirical refutation of the prevailing assumption that interactive, step-by-step proof search is necessary for competitive neural theorem proving performance. Prior to this work, the dominant paradigm — exemplified by GPT-f, Proof Artifact Co-Training, Hypertree Proof Search, ReProver, and COPRA — treated interactive search as essential: the model proposes a tactic, the proof assistant verifies it and returns the new proof state, and the model proposes the next tactic based on the updated state. This architecture was justified by the intuition that the search space for complete proofs is too vast for single-pass generation to succeed, and that the verifier's feedback at each step is necessary to keep the model on track.

DeepSeek-Prover challenges this assumption directly. Using only whole-proof generation — a single forward pass producing the entire proof — the model achieves 46.3% on miniF2F-test at 64 samples and 52% cumulatively (Table 1). This surpasses every interactive search method reported in the table, including Hypertree Proof Search (41.0% at 64×5000 search steps with a 600M-parameter model), Curriculum Learning (36.6% at 64×8×512 with an 837M-parameter model), and COPRA with GPT-4 (26.6% at 60 attempts). The comparison is not perfectly controlled — the interactive methods use smaller models and different generation budgets — but the magnitude of the gap (5-20 percentage points) and the fact that DeepSeek-Prover achieves this without any interactive feedback make the result striking.

The insight is not that interactive search is obsolete — the paper does not claim this, and for harder problems (FIMO, where DeepSeek-Prover solves only 5/148), interactive search might well be necessary. The insight is rather that with sufficient task-specific training data, single-pass generation can outperform search-guided generation, because the model internalizes proof strategies that would otherwise need to be explored through expensive trial and error. This is analogous to the difference between a chess player who calculates variations at the board (search) and one who recognizes patterns from thousands of studied games and plays intuitively (learned generation). Both are valid approaches, and their relative effectiveness depends on how much relevant training data the model has internalized.

This finding has practical significance for the design of neural theorem provers. Interactive search requires maintaining a connection between the LLM and the proof assistant, handling proof state serialization, managing backtracking, and paying the latency cost of multiple model calls per proof. Whole-proof generation eliminates all of this infrastructure: one model call, one verification check. If whole-proof generation can achieve competitive or superior performance with sufficient training data — as this paper demonstrates for competition-level problems on miniF2F — then the field's heavy investment in search infrastructure may be partially misallocated. The bottleneck is data, not search algorithms.

The evidence in Table 1 directly supports this claim through the comparison between DeepSeek-Prover (whole-proof, 7B parameters, 52% cumulative on miniF2F-test) and the best tree search method (Hypertree Proof Search, 600M parameters, 41.0% on miniF2F-test). The fact that a 7B model with whole-proof generation outperforms a tree search method with comparable or greater computational budgets (64×5000 = 320,000 search steps for Hypertree vs. up to 65,536 generation attempts for DeepSeek-Prover) suggests that the learned proof strategies from 8 million training examples more than compensate for the lack of interactive feedback. This is not an incremental improvement over prior whole-proof methods — it's a roughly 2× improvement over GPT-4 (23.0% → 46.3% at 64 samples) and a new state of the art on the benchmark — and it reframes the central challenge of neural theorem proving from "how do we search more efficiently" to "how do we generate better training data."

5. Experimental Analysis

Evaluation Methodology

• Dataset. The primary evaluation benchmark is miniF2F (Zheng et al., 2021), a cross-system formal mathematics benchmark consisting of 244 validation and 244 test problems spanning basic arithmetic through competition-level problems from the AIME, AMC, and IMO — specifically the Lean 4 version released by the LeanDojo project. The secondary benchmark is FIMO (Liu et al., 2023), comprising 148 formal problems sourced from the IMO shortlist translated into Lean 4.
• Base model(s). All experiments use DeepSeekMath-Base 7B (Shao et al., 2024), a decoder-only transformer pre-trained on 120 billion math-related tokens, chosen because its mathematical pretraining provides a strong inductive bias for formal reasoning. For baselines, GPT-3.5 and GPT-4 (specifically the GPT-4-turbo 0409 version) are evaluated as frontier general-purpose models. Other compared baselines use models ranging from 229M to 34B parameters.
• Metrics. The primary metric is pass@k — the fraction of problems for which at least one valid proof is discovered among the first k proof candidates sampled from the model, where a proof is "valid" if it passes verification by the Lean 4 proof assistant. A cumulative metric is also reported, representing the aggregate pass rate across all samples generated regardless of k. For FIMO, the metric is simply the number of problems proved out of 148 at specific generation budgets.
• Baselines. The paper compares against several families of methods from prior work. Tree search methods: COPRA with both GPT-3.5 and GPT-4 (Thakur et al., 2023), Proof Artifact Co-Training with an 837M model (Han et al., 2021), ReProver with a 229M model (Yang et al., 2024), Llemma with 7B and 34B models (Azerbayev et al., 2023), Curriculum Learning with an 837M model (Polu et al., 2022), and Hypertree Proof Search with a 600M model (Lample et al., 2022). Whole-proof generation methods: GPT-4-turbo 0409 and DeepSeekMath-Base 7B (the pre-trained model without synthetic data fine-tuning), both generating complete proofs in a single pass followed by Lean 4 verification.
• Generation budget / compute accounting. For whole-proof generation baselines and DeepSeek-Prover, the budget is measured in number of independent proof candidates sampled (1 for greedy, up to 65,536 for maximum sampling). For tree search methods, the budget is reported in the notation a × b × c or a × b depending on the specific search configuration — typically representing some combination of the number of search episodes, expansion steps per episode, and parallel branches — as reported in the original papers and transcribed into Table 1. No attempt is made to normalize FLOPs or wall-clock time across methods; the comparison is heterogeneous in compute units.
• Cross-validation / statistical protocol. No cross-validation or statistical significance testing is reported. Results are presented as point estimates (percentages on miniF2F, raw counts on FIMO) without confidence intervals. The miniF2F split into validation and test sets (244 each) is used for reporting (both are shown in Table 1), but there is no k-fold stratification or significance testing across random seeds.

Main Quantitative Results

Whole-Proof Generation on miniF2F

The central result is DeepSeek-Prover's performance on miniF2F-test across varying generation budgets, reported in Table 1. The headline numbers:

• Greedy (1 sample): 30.0% accuracy — meaning the model produces a correct proof on its first attempt for nearly one-third of the 244 test problems.
• 64 samples: 46.3% accuracy — a +16.3 percentage point improvement over greedy, indicating substantial gains from modest sampling.
• 128 samples: 46.3% accuracy — identical to 64 samples, revealing a plateau where additional samples within this range do not surface new correct proofs.
• 8,192 samples: 48.8% accuracy — a +2.5 percentage point improvement beyond the plateau.
• 65,536 samples: 50.0% accuracy — a +1.2 percentage point improvement, reaching half of all test problems.
• Cumulative: 52.0% accuracy — aggregating across all sample budgets captures an additional 2.0 percentage points beyond the 65,536-sample result, representing problems where correct proofs exist in the sampling distribution but are extremely rare.

The comparison against baselines at comparable sampling budgets (Table 1, "Whole-Proof Generation Methods" section) is stark:

• GPT-4-turbo 0409 at 64 samples: 23.0% on miniF2F-test — DeepSeek-Prover achieves more than double this at the same budget (46.3%), despite DeepSeek-Prover having only 7B parameters versus GPT-4's vastly larger (undisclosed) parameter count.
• GPT-4-turbo 0409 cumulative: 25.4% on miniF2F-valid (vs. DeepSeek-Prover's 60.2%) and 22.95% (23.0% rounded) on miniF2F-test (vs. 52.0%).
• DeepSeekMath-Base 7B at 128 samples: 27.5% on miniF2F-test — the pre-trained model without synthetic data fine-tuning performs only modestly better than GPT-4, demonstrating that the 120B-token mathematical pretraining alone is insufficient for competitive formal proof generation. DeepSeek-Prover at 128 samples achieves 46.3%, a +18.8 percentage point improvement attributable entirely to the synthetic data fine-tuning.

The comparison against tree search methods (Table 1, "Tree Search Methods" section) shows DeepSeek-Prover outperforming all listed interactive methods:

• Hypertree Proof Search (the best tree search method): 41.0% on miniF2F-test at 64×5000 search steps with a 600M-parameter model. DeepSeek-Prover at 64 samples (46.3%) surpasses this by +5.3 percentage points using whole-proof generation with a 7B model.
• Curriculum Learning (best configuration, 64×8×512 with an 837M model): 36.6% on miniF2F-test. DeepSeek-Prover outperforms by +9.7 percentage points at 64 samples.
• COPRA with GPT-4 (1×60): 26.6% on miniF2F-test. DeepSeek-Prover at comparable budgets outperforms by approximately +20 percentage points.

On miniF2F-valid (the validation split), DeepSeek-Prover achieves 60.2% cumulative, surpassing Hypertree Proof Search's 58.6% cumulative on the same split — the only tree search method that comes close.

FIMO Benchmark Results

On the substantially harder FIMO benchmark (148 IMO shortlist problems in Lean 4), the paper reports (Section 4.2, "Results on FIMO"):

• 100 attempts per theorem: DeepSeek-Prover solves 4 out of 148 problems, while GPT-4 solves 0 out of 148. This is the first demonstration of a neural prover making non-trivial progress on FIMO — a benchmark explicitly composed of IMO-level problems.
• 4,096 attempts per theorem: DeepSeek-Prover solves 5 out of 148 problems — one additional theorem beyond the 100-attempt result, indicating that for the hardest problems, increasing the sampling budget by 40× yields marginal returns (+1 theorem). The paper does not report a sweep of intermediate budgets, so the exact scaling curve between 100 and 4,096 is unknown.

The FIMO results provide evidence of capability on problems substantially beyond the competition-level difficulty of miniF2F, but the absolute performance (5/148 = 3.4%) underscores that formal IMO-level theorem proving remains largely unsolved.

Scaling of Synthetic Data Volume

Table 5 reports the pass@128 on miniF2F as a function of the fraction of the 8 million synthetic proof data points used for training. The paper describes a "clear correlation between dataset size and model efficacy" (Section 4.3.4) — performance improves as an exponentially larger fraction of the synthetic data is included. Specific numbers are not quoted in the text, but the table demonstrates that the full 8 million dataset is necessary to achieve the reported 50.0% pass@128 performance, confirming that data scale, not just data quality, is a critical driver of the final results.

Ablation Studies and Robustness Checks

Large-scale autoformalization vs. mathlib-only data (Table 2): Models trained on synthetic proofs from autoformalized data significantly outperform those trained solely on formal proofs derived from human-authored theorems in Lean 4's mathlib. This confirms that the autoformalization pipeline adds training signal beyond what is available in the existing formal mathematics library, and that the diversity of the informal competition problem corpus translates into improved prover capability. The specific pass rates are reported in Table 2 but not quoted numerically in the text — the paper states that "models trained with our autoformalized data significantly outperform those trained solely with mathlib data" (Section 4.3.1).

Formal statement quality scoring (Table 3): Models fine-tuned on proof data associated with high-scoring formal statements outperform models trained on low-scoring proof data by 4.5 percentage points on miniF2F pass@128. This validates that the quality scoring model (the chain-of-thought rubric described in Section 3.2) meaningfully separates higher-quality from lower-quality formalizations, and that training on higher-quality formalizations yields better downstream provers. The 4.5% gap is the quantitative evidence for the scoring model's effectiveness.

Iterative enhancement (Table 4): Across three successive training iterations of the full pipeline (autoformalization → filtering → proof generation → fine-tuning → repeat), miniF2F pass@128 improves from 32.3% → 42.0% → 50.0%. The gain from iteration 1 to 2 (+9.7 percentage points) is slightly larger than from iteration 2 to 3 (+8.0 points), indicating diminishing but still substantial returns. The ablation demonstrates that the iterative self-improvement loop is essential — training on only the first iteration's data yields 32.3%, while each subsequent iteration adds data that meaningfully improves the model beyond what the previous iteration achieved.

Scaling synthetic data (Table 5): As described above, performance on miniF2F pass@128 improves monotonically with the fraction of the 8-million-example dataset used. The paper emphasizes that this is an "exponential increase" in dataset size (Section 4.3.4), though the exact functional form of the scaling curve — whether logarithmic, power-law, or otherwise — is not characterized beyond reporting the table values. The key finding is that 8 million examples yield substantially better performance than smaller subsets, confirming that data quantity matters and that the full dataset was necessary to reach the reported state-of-the-art numbers.

Critical Assessment

Claim: "Our model outperforms GPT-4 and other methods on benchmarks like miniF2F"

Supported, but with important caveats about the comparison. The numbers in Table 1 are unambiguous: DeepSeek-Prover at 46.3% (64 samples) substantially exceeds GPT-4 at 23.0% (64 samples) on miniF2F-test. However, the nature of the comparison requires scrutiny. GPT-4 is evaluated as a zero-shot or few-shot whole-proof generator without any formal-proof-specific fine-tuning — it relies entirely on whatever formal mathematics knowledge was incidentally acquired during its massive general-purpose pretraining. DeepSeek-Prover, by contrast, is fine-tuned on 8 million domain-specific theorem-proof pairs. The comparison therefore tests "specialized fine-tuned model" against "general-purpose model," not "superior architecture" against "larger architecture." The paper does not report what happens if GPT-4 is fine-tuned on the same 8 million synthetic examples (which may be practically infeasible given GPT-4's closed nature, but would be the most direct comparison of model capability), nor does it fine-tune any other open model (e.g., Llemma 7B or 34B) on the synthetic dataset to isolate the contribution of the data from the contribution of DeepSeekMath-Base's specific pretraining.

A further subtlety: Table 1 reports GPT-4 with 64 samples, but DeepSeek-Prover at the same budget achieves 46.3%. However, Table 1 also reports Llemma 7B (a model of comparable scale to DeepSeek-Prover) at 26.2% pass@1×3200 on miniF2F-test — but this is with interactive search (1×3200 steps), not whole-proof generation, and the model is not fine-tuned on the synthetic dataset. There is no direct comparison: what would Llemma 7B achieve if fine-tuned on the same 8 million examples and evaluated with whole-proof generation at 64 samples? If it matched or exceeded DeepSeek-Prover's performance, then the key contribution is the dataset, not the model. If it underperformed, then DeepSeekMath-Base's pretraining provides a complementary advantage. The paper cannot distinguish these explanations because the cross-model fine-tuning experiment is absent.

On FIMO, the claim that DeepSeek-Prover "successfully proved 5 out of 148 problems... while GPT-4 failed to prove any" is supported as a raw empirical fact. However, with only 5 positive examples (and 0 for GPT-4), the comparison has limited statistical resolution. A single lucky sample could account for the difference — the paper does not report whether the 5 proofs hold up under repeated runs with different random seeds, nor whether GPT-4 was given the same 4,096-attempt budget (the text only mentions GPT-4 at 100 attempts, where it also achieved 0).

Claim: "Large-scale synthetic data significantly enhances theorem-proving capabilities"

Supported. The evidence is multi-pronged and internally consistent. The comparison between DeepSeekMath-Base 7B (27.5% at 128 samples, no synthetic data fine-tuning) and DeepSeek-Prover (46.3% at 64 samples, with synthetic data fine-tuning) isolates the effect of the synthetic data training — a +18.8 percentage point gain with fewer samples, which is a strong signal. The ablation in Table 2 (autoformalized data vs. mathlib-only data) confirms that the synthetic data adds value beyond what is available in existing formal corpora. Table 5 (scaling with dataset size) demonstrates that more synthetic data yields better performance. Table 4 (iterative enhancement) shows that successive rounds of synthetic data generation compound the gains. The consistency across these independent ablations — all pointing toward synthetic data as the primary driver — makes the claim robust.

However, the paper cannot fully disentangle the effect of quantity from the effect of diversity. The synthetic dataset contains 8 million examples spanning multiple mathematical domains (algebra, number theory, combinatorics, geometry, statistics) and multiple problem types. The mathlib data, while human-curated and high-quality, may cover a narrower or different distribution. The improvement in Table 2 could therefore be due to better domain coverage rather than the synthetic data's inherent quality or scale per se. A controlled ablation that matched the domain distribution and problem types of mathlib and the synthetic data would be needed to isolate this — such an experiment is not reported.

Claim: "Iterative self-improvement progressively increases model performance"

Supported, with diminishing returns evident. Table 4 provides the core evidence (32.3% → 42.0% → 50.0%), and the monotonic improvement across iterations is clear. However, the paper does not report what happens beyond iteration 3 — does performance saturate at 50%, or would further iterations continue to yield marginal gains? The text states the cycle "continues until no further gains are observed" (Section 3.4), implying additional iterations were run but the gains became negligible, yet no data beyond iteration 3 is presented. This matters for practical replication: if iteration 4 adds only 0.5 percentage points at significant computational cost, the optimal stopping point would be iteration 3; if it adds 3 more points, the full benefit of the method would be underestimated. The absence of this data — and the absence of a cost-benefit analysis of each iteration's compute requirements — limits the practical guidance the paper offers.

Additionally, the iterative enhancement results conflate two effects: (1) each iteration adds more training data (the cumulative dataset grows), and (2) each iteration's data is generated by a stronger model and is presumably higher quality. Table 4 cannot distinguish whether the gains come from having 3× more data versus having higher-quality data from a stronger generator. A "data quality vs. data quantity" ablation — e.g., training on 8 million first-iteration examples vs. 8 million mixed-iteration examples — is not reported and would strengthen the paper's claim about iterative quality improvement specifically.

Claim: "Whole-proof generation achieves state-of-the-art performance, surpassing tree search methods"

Supported with the caveat that the comparison is not compute-controlled. The numbers in Table 1 (DeepSeek-Prover: 46.3% at 64 whole-proof samples vs. Hypertree Proof Search: 41.0% at 64×5000 search steps) are genuine state-of-the-art improvements. However, the comparison has no common compute metric. A single whole-proof generation pass from a 7B model and a single search step from a 600M model have vastly different FLOPs. It is possible — the paper provides no data to rule this out — that Hypertree Proof Search with 64×5000 steps on a 600M model uses less total compute than DeepSeek-Prover with 64 whole-proof generations on a 7B model. If true, the tree search method might still be more compute-efficient even if it achieves lower absolute accuracy. The paper does not attempt any FLOPs normalization or wall-clock comparison, so the claim of "surpassing" is purely in terms of benchmark accuracy, not compute efficiency or practical deployability.

A second caveat: the tree search methods in Table 1 use models of 229M to 837M parameters (with the exception of Llemma at 7B/34B, which uses 1×3200 search steps). DeepSeek-Prover at 7B parameters is 8-30× larger than most of the tree search models. Whether tree search with a comparably sized 7B model — fine-tuned on the same synthetic dataset — would outperform whole-proof generation is not tested. The paper's claim that whole-proof generation "surpasses" tree search is therefore a claim about the specific models and configurations evaluated, not a general architectural superiority claim. The results convincingly demonstrate that whole-proof generation with a sufficiently fine-tuned model can be competitive with or better than smaller models using interactive search, but they do not rule out the possibility that interactive search with a similarly fine-tuned 7B model would be even stronger.

Claim: "Quality filtering removes low-quality statements and improves downstream performance"

Qualitatively supported, quantitatively thin. The case study in Section 5.2 shows a concrete example of hypothesis rejection detecting an inconsistent formalization (the matrix determinant example with over-universal quantification), which is compelling as an existence proof. The 4.5 percentage point gap between high-score and low-score proof data (Table 3) confirms that the scoring model's rankings are predictive of downstream value. However, several pieces of quantitative evidence are missing:

• What fraction of the 18% of discarded statements (the difference between 869,659 input problems and 712,073 filtered statements) was removed by quality scoring vs. hypothesis rejection? Without this breakdown, the relative importance of the two mechanisms cannot be assessed.
• What is the false positive rate of hypothesis rejection — i.e., how many correctly formalized statements were incorrectly flagged as having inconsistent hypotheses because the model failed to prove False from consistent hypotheses? The paper mentions none.
• What is the false negative rate — how many statements with genuinely inconsistent hypotheses passed the hypothesis rejection filter because the inconsistency was too subtle for the current model to detect? Again, no quantification.
• How many of the 712,073 filtered statements turned out to be unprovable during the subsequent proof generation phase (i.e., neither Stream 1 nor Stream 2 succeeded within the budget)? This would indicate the precision of the combined filtering pipeline.

Without these numbers, the filtering module is demonstrated to help (Table 3) but its operating characteristics — precision, recall, failure modes — are opaque.

Missing Experiments That Would Strengthen the Paper

1. Fine-tuning an alternative base model on the synthetic dataset. If the 8 million synthetic examples were used to fine-tune Llemma 7B (the most comparable open model), would it achieve similar performance to DeepSeek-Prover? If yes, the dataset is the primary contribution and the choice of base model matters less. If no, DeepSeekMath-Base's pretraining confers a specific advantage that interacts with the synthetic data. Either outcome would be informative; the absence of this experiment leaves the relative contributions of data vs. pretraining unresolved.

2. Performance by mathematical domain. The paper states that autoformalization focuses on algebra and number theory (Section 3.1). miniF2F contains problems from multiple domains. Does DeepSeek-Prover's improvement concentrate in algebra and number theory (where the synthetic data is strongest) with minimal improvement in geometry or other areas? A domain-stratified breakdown would reveal whether the synthetic data's benefits generalize or are domain-specific.

3. Compute cost of the full pipeline. The paper reports no FLOPs, GPU-hours, or dollar costs for the autoformalization, filtering, proof generation, and iterative fine-tuning of the 8 million examples. This makes it impossible for other researchers to assess the practicality of replicating the approach. If generating the dataset required millions of GPU-hours, the method may only be feasible for well-resourced industrial labs — which is fine, but should be stated transparently.

4. Statistical confidence on miniF2F results. The miniF2F-test set has 244 problems. A difference of a few percentage points (e.g., 46.3% vs. 41.0%) corresponds to ~12-13 problems. Without confidence intervals (e.g., bootstrapped over the test set), it is difficult to assess whether the gap between DeepSeek-Prover and Hypertree Proof Search is statistically reliable or could be explained by test-set variance.

5. Interactive search with the fine-tuned model. Given that DeepSeek-Prover achieves 30% greedy accuracy on miniF2F-test, what happens if the same model is used in an interactive search setup (à la GPT-f or Hypertree Proof Search) rather than whole-proof generation? If interactive search adds significant further gains, then the paper's implicit message that whole-proof generation is sufficient would be misleading. If it adds nothing, that would be a strong result reinforcing the paper's architectural choice. The absence of this experiment leaves the complementarity (or lack thereof) between synthetic data fine-tuning and interactive search unexplored.

6. FIMO with GPT-4 at 4,096 attempts. The paper reports GPT-4 at 0/148 on FIMO, but the generation budget for GPT-4 is not stated in the FIMO section (only that it "failed to prove any"). If GPT-4 was limited to 100 attempts while DeepSeek-Prover was given 4,096, the comparison is budget-asymmetric. Showing GPT-4's performance at 4,096 attempts would clarify whether the improvement on FIMO is due to the synthetic data fine-tuning or simply due to a larger sampling budget being allocated to the fine-tuned model.

Genuine Weaknesses

The most significant weakness is the single-base-model design. All results are with DeepSeekMath-Base 7B. The paper's central claim is about synthetic data and the iterative pipeline, not about DeepSeekMath specifically, but without testing the pipeline on a different base model, the claim's generality is unproven. If the pipeline depends on DeepSeekMath-Base's specific pretraining distribution (e.g., its exposure to Lean-like syntax during the 120B-token math pretraining), then the method may not transfer straightforwardly to other base models.

A second weakness is the opacity of the difficulty estimation for the autoformalization and proof generation pipeline. The paper does not characterize which informal problems autoformalize successfully, which yield provable formal statements, or which yield proofs within the generation budget. The yield analysis (869,659 → 712,073 → 8 million theorem-proof pairs) aggregates over all iterations and difficulty levels, obscuring potentially important structure — for example, if autoformalization works well for algebraic identities but poorly for combinatorial existence proofs, the synthetic dataset would have a hidden domain bias that the evaluation on miniF2F (which is domain-mixed) might not reveal.

A third weakness is the absence of contamination analysis. The synthetic data is generated from an informal problem corpus scraped from online competition resources. Some of these problems may overlap with miniF2F or FIMO in content — if the model saw natural language versions of miniF2F problems during training (even if the formalizations differed), the evaluation overestimates generalization. The paper mentions no decontamination protocol.

Finally, the FIMO results, while positive, are too sparse to draw strong conclusions. Five problems out of 148 is a hit rate of 3.4%, and the paper provides no analysis of which five problems were solved, whether they share common characteristics (e.g., all algebra, all from a specific difficulty tier), or whether the solved problems were among the easier or harder FIMO entries. Five successes out of 148 could represent genuine progress on a specific subclass of problems or simply lucky sampling on problems that happened to be within the model's reach. A qualitative analysis of the solved vs. unsolved FIMO problems would substantially strengthen the claim.

Summary of Conditional Claims

• "DeepSeek-Prover outperforms GPT-4": Holds on miniF2F (46.3% vs. 23.0% at 64 samples, Table 1). Holds on FIMO (5/148 vs. 0/148, but with budget asymmetry caveats). The comparison is between a domain-specialized fine-tuned model and a general-purpose model — not between two comparably fine-tuned models.
• "Synthetic data significantly enhances theorem-proving": Holds for DeepSeekMath-Base 7B on competition-level algebra and number theory problems. Generalization to other base models, other mathematical domains, and harder theorems (IMO-level) is not established but partially supported by FIMO results.
• "Iterative enhancement compounds gains": Holds across three iterations with DeepSeekMath-Base 7B (Table 4). Whether the compounding continues beyond three iterations or generalizes to other base models and problem domains is untested.
• "Whole-proof generation surpasses tree search": Holds on miniF2F-test for the specific models and configurations compared (Table 1). Not established as a general architectural superiority — would require compute-controlled comparisons or interactive search applied to the fine-tuned DeepSeek-Prover.

6. Limitations and Trade-offs

Limited Mathematical Domain: Algebra and Number Theory Only

The assumption or constraint. The paper deliberately restricts autoformalization and proof generation to "high school and undergraduate-level competition problems, with a particular emphasis on algebra and number theory, and to a lesser extent, combinatorics, geometry, and statistics" (Section 3.1). The justification is pragmatic: problems with "explicit conditions and well-defined goals are typically easier to formalize compared to advanced mathematical topics that necessitate intricate definitions and constructions" (Section 3.1). This means the pipeline does not attempt to formalize problems requiring deep theoretical machinery — real analysis with epsilon-delta arguments, topology, abstract algebra (groups, rings, fields beyond basic properties), category theory, or any area where the formalization would require generating correct definitions of sophisticated mathematical structures.

The consequence. DeepSeek-Prover's capabilities are bounded by the domain coverage of its training data. The model has never seen formal proofs about continuity, compactness, group homomorphisms, or vector spaces beyond basic linear algebra. A practitioner attempting to use DeepSeek-Prover for real analysis or abstract algebra would encounter a model with no relevant training signal — it would either fail to produce valid proofs or hallucinate plausible-sounding but incorrect Lean 4 syntax. The paper's evaluation on miniF2F and FIMO partially reflects this: miniF2F includes problems from multiple domains (the paper does not provide a domain-stratified breakdown of successes), but FIMO — where the model solves only 5/148 problems — may contain a higher proportion of problems outside the algebra/number theory comfort zone. However, the paper provides no domain analysis of the solved vs. unsolved FIMO problems, so this remains speculative.

What evidence exists in the paper. The scope limitation is stated explicitly in Section 3.1: the paper "primarily examines high school and undergraduate-level competition problems, with a particular emphasis on algebra and number theory." The ablation in Table 2 (autoformalized data vs. mathlib-only data) does not break down performance by mathematical domain, so there is no quantitative evidence on how much of the improvement is concentrated in algebra/number theory versus spreading across all miniF2F domains. The paper's conclusion acknowledges this, stating that future work will "aim to expand the diversity of mathematical problems addressed, enhancing the general applicability of our methods in ATP" (Section 6).

Mitigation status. Not addressed in the current work. The limitation is fundamental to the training data construction: expanding to new domains would require either (a) an informal problem corpus covering those domains, (b) an autoformalizer capable of generating correct formalizations of advanced concepts (which the current model cannot do), or (c) seed formal data from mathlib in those domains to bootstrap the autoformalizer. The paper frames this purely as future work.

Difficulty Estimation Cost Is Unaccounted for in the Pipeline

The assumption or constraint. The iterative pipeline requires running autoformalization on 869,659 informal problems, quality-scoring each of the resulting 8 million+ candidate formal statements (across iterations), running dual-stream proof search with up to $k$ attempts per statement per stream, and fine-tuning a 7B model on the accumulated data for multiple iterations. The paper reports no compute budget for this process — no GPU-hours, no FLOPs estimates, no wall-clock time, and no dollar cost. Section 4.1 reports the fine-tuning configuration (global batch size 512, learning rate 1×10−4, 6,000 warmup steps) but only for the final fine-tuning stage, not for the full iterative pipeline. The cost of generating the 8 million examples — including the dual-stream proof search, which may expend $2k$ proof attempts per statement, each involving a forward pass through a 7B model followed by Lean 4 verification — is entirely opaque.

The consequence. This opacity has two practical implications. First, reproducibility is compromised: a research group attempting to replicate the pipeline cannot estimate the required compute budget, making resource planning impossible. Second, the headline efficiency claim is incomplete: the paper demonstrates that whole-proof generation with a 7B model at 64 samples achieves 46.3% on miniF2F-test, outperforming tree search methods — but this comparison excludes the massive one-time compute investment required to generate the synthetic dataset. If generating the 8 million examples required, say, 10,000 GPU-hours, then the total cost (dataset generation + inference) might exceed the cost of simply running interactive search with a 600M model for many more steps. The paper cannot refute this because it provides no numbers. A practitioner deciding between "invest in synthetic data generation" and "invest in better search algorithms" receives no quantitative guidance.

What evidence exists in the paper. There is none. The paper does not mention compute cost anywhere — not in the main text, not in the appendices, not even as a qualitative characterization ("the pipeline required approximately X GPU-days"). The fine-tuning hyperparameters in Section 4.1 are the only quantitative resource information provided, and they cover only one component of the iterative cycle.

Mitigation status. Completely unaddressed. This is a significant gap because the paper's central argument is about scalability — that large-scale synthetic data is the path forward for neural theorem proving. Without cost transparency, the reader cannot evaluate whether the approach scales economically or only technically.

No Evidence of Generalization Beyond the Single Base Model

The assumption or constraint. All experiments — the autoformalization pipeline, the iterative enhancement, the quality filtering, the proof generation, and the final evaluation — use exactly one base model: DeepSeekMath-Base 7B (Shao et al., 2024), a decoder-only transformer pre-trained on 120 billion math-related tokens. The paper does not apply the synthetic data pipeline to any other base model — not a general-purpose model (e.g., LLaMA, Mistral), not a code-specialized model (e.g., CodeLlama), not a differently-sized variant of DeepSeekMath, and not an alternative math-specialized model (e.g., Llemma 7B or 34B). The paper's claims about the synthetic dataset's value and the iterative pipeline's effectiveness are therefore conditional on the specific pretraining distribution of DeepSeekMath-Base.

The consequence. The paper cannot distinguish between two competing explanations for DeepSeek-Prover's performance: (a) the synthetic data pipeline is generally effective and would improve any competent base model, or (b) the synthetic data pipeline works because DeepSeekMath-Base's pretraining on 120 billion math-specific tokens already provides strong representations of mathematical concepts and possibly some exposure to Lean-like formal syntax, and the synthetic data merely fine-tunes these existing capabilities. If (b) is true, a research group attempting to replicate the approach with, say, Llemma 7B (which was pre-trained on Proof-Pile-2, a different mathematical corpus) might see substantially smaller gains, because the base model's pretraining distribution does not align as well with the synthetic data's formal syntax and proof strategies. Conversely, if (a) is true, the synthetic dataset itself is the primary contribution and should be evaluated independently of the base model.

This matters for practical deployment. An organization with an existing investment in a particular base model (e.g., LLaMA fine-tuned for code generation) cannot determine from this paper whether the synthetic data approach would work for them, or whether they would need to switch to DeepSeekMath-Base specifically — which may have different licensing, deployment, or infrastructure implications.

What evidence exists in the paper. Table 1 includes DeepSeekMath-Base 7B as a baseline (27.5% on miniF2F-test at 128 samples, whole-proof generation without synthetic data fine-tuning). This shows that the base model alone is not competitive, and the synthetic data fine-tuning adds substantial value (+18.8 percentage points). However, this is a within-model comparison — it does not test the interaction between pretraining and synthetic data across models. The paper cites Llemma (Azerbayev et al., 2023) in Table 1 as a tree search baseline (7B and 34B variants at 1×3200 search steps), but never fine-tunes Llemma on the synthetic dataset. The ablation in Table 2 compares synthetic data against mathlib-only data but only within the DeepSeekMath-Base model family.

Mitigation status. Not addressed. The paper does not acknowledge this as a limitation, does not discuss model-specific pretraining effects, and does not suggest cross-model experiments as future work. The conclusion mentions releasing the dataset and model to "facilitate further research" (Section 6), which would enable the community to perform these cross-model experiments, but the paper itself provides no evidence of generalization.

Hardest Problems Remain Essentially Unsolved

The assumption or constraint. The paper's evaluation on FIMO — the harder of the two benchmarks, comprising 148 IMO shortlist problems in Lean 4 — reveals a sharp capability ceiling. DeepSeek-Prover solves only 5 out of 148 problems even with 4,096 attempts per theorem (Section 4.2), yielding a success rate of ~3.4%. GPT-4 solves 0 out of 148. The paper does not analyze the 5 solved problems to determine whether they share common characteristics (e.g., all simple algebra, all from a specific difficulty tier within FIMO, all requiring only basic tactics) or whether they represent genuinely diverse IMO-level reasoning.

The consequence. The synthetic data approach appears to saturate well below the level needed for IMO-competition theorem proving. The improvement from 100 attempts (4/148 solved) to 4,096 attempts (5/148 solved) is marginal — a 40× increase in compute yields only one additional proof. This suggests that for problems at FIMO difficulty, neither additional sampling nor the current synthetic data distribution provides a path to significant further improvement. The bottleneck is likely the capability ceiling of the base model rather than data quantity: if the model's 7B-parameter architecture and pretraining do not encode the reasoning patterns needed for IMO-level problems (e.g., complex induction schemes, non-trivial case analysis, creative lemma application), no amount of fine-tuning on competition-level synthetic data will create these capabilities from scratch.

This limitation is particularly consequential because it bounds the approach's applicability. If a practitioner's goal is to formalize routine undergraduate mathematics (linear algebra identities, basic number theory, trigonometric manipulations), DeepSeek-Prover at 46.3% miniF2F accuracy is plausibly useful. If the goal is to assist with research-level mathematics or IMO training, a 3.4% success rate on FIMO is far below practical utility — and the plateau suggests that simply generating more synthetic data of the same kind will not close the gap.

What evidence exists in the paper. The FIMO results are reported in Section 4.2 ("Results on FIMO") with the specific numbers: 4/148 at 100 attempts, 5/148 at 4,096 attempts. No analysis of the solved problems is provided — the paper lists which theorems were proved only in Appendix A.3.2, with two example proofs shown (an IMO 2009 functional equation problem and an IMO 2016 inequality problem). The miniF2F scaling curve (Table 1) shows similar saturation behavior: performance plateaus at 46.3% from 64 to 128 samples, and only slowly increases to 50.0% at 65,536 samples. This pattern — rapid initial gains followed by a long tail of diminishing returns — is consistent with the model reaching the limits of what the synthetic data distribution covers.

Mitigation status. The paper acknowledges this in the conclusion only indirectly: "Currently, our work mainly focuses on algebra and number theory at the middle school and undergraduate levels. In future work, we will aim to expand the diversity of mathematical problems addressed" (Section 6). This framing treats the limitation as a domain diversity issue rather than a difficulty ceiling, but the FIMO results (where the domain is still competition mathematics, just at a higher difficulty tier) suggest the ceiling is about problem complexity, not just domain breadth. The paper proposes no mechanism for breaking through this ceiling — e.g., incorporating search during inference, scaling to larger base models, or generating synthetic data specifically at IMO difficulty.

Inconsistent Compute Comparison Between Whole-Proof Generation and Tree Search

The assumption or constraint. Table 1 compares DeepSeek-Prover's whole-proof generation performance against tree search methods (Hypertree Proof Search, Curriculum Learning, COPRA) using the generation budgets reported in the original papers — but these budgets measure fundamentally different things. For DeepSeek-Prover, "64" means 64 independent complete proofs generated in parallel and each verified once. For Hypertree Proof Search, "64×5000" means 64 independent search episodes, each exploring up to 5,000 proof steps through the tree, with each step requiring a model call to generate a tactic, a verifier call to check it, and state serialization/deserialization. The computational cost of these two protocols is incomparable without a common metric (FLOPs, GPU-hours, wall-clock time), which the paper does not provide.

The consequence. The claim that DeepSeek-Prover "surpasses" tree search methods (Section 4.2, Table 1) is a claim about benchmark accuracy, not about compute efficiency. It is possible — the paper provides no data to rule this out — that Hypertree Proof Search with a 600M model and 64×5000 search steps uses less total compute than DeepSeek-Prover with a 7B model and 64 whole-proof generations, because (a) the 600M model is ~12× smaller than DeepSeek-Prover, making each forward pass cheaper, and (b) many search steps in Hypertree Proof Search may be pruned early or share prefixes, reducing effective depth. If Hypertree Proof Search uses less compute to achieve 41.0% than DeepSeek-Prover uses to achieve 46.3%, then the choice between methods involves a compute-accuracy tradeoff that the paper's Table 1 obscures.

A further issue: the tree search baselines use models at 229M–837M parameters (with the exception of Llemma at 7B/34B, but Llemma at 1×3200 is a single-search-episode configuration, not a deep search). DeepSeek-Prover at 7B parameters is 8–30× larger than most of these baselines. The paper does not evaluate what happens when a comparably sized 7B model is used with tree search — the comparison is between "large model + whole-proof generation + synthetic data" and "small model + tree search + less synthetic data," which confounds model scale and fine-tuning data with the architectural choice of generation strategy.

What evidence exists in the paper. None. The paper reports no FLOPs counts, no GPU-hours for generation, no latency measurements, and no parameter-count-normalized comparisons. Table 1 reports generation budgets as reported in the original papers, without attempting to harmonize them into a common compute metric. The paper does not acknowledge this as a limitation.

Mitigation status. Completely unaddressed. The paper treats the generation budget numbers as directly comparable, which they are not. A reader cannot determine from this paper whether DeepSeek-Prover's whole-proof generation is genuinely more compute-efficient than tree search, or merely uses a larger model and more extensive fine-tuning to achieve higher accuracy at potentially higher cost.

The Dataset Size Benefit May Be Partially Attributable to Domain Diversity, Not Scale Per Se

The assumption or constraint. The paper claims that the 8 million synthetic theorem-proof pairs drive DeepSeek-Prover's performance, supported by the scaling ablation in Table 5 (performance improves with larger fractions of the dataset) and the comparison to mathlib-only training in Table 2 (synthetic data outperforms human-authored mathlib data). However, these comparisons confound quantity (8 million examples vs. mathlib's tens of thousands) with domain diversity. The synthetic dataset spans problems from algebra, number theory, combinatorics, geometry, and statistics at competition levels. Mathlib, while human-curated, may have a different — possibly narrower or differently distributed — domain coverage. The improvement from using synthetic data could therefore be due to the model seeing a wider variety of mathematical concepts and proof patterns, not the sheer number of examples.

The consequence. If domain diversity is the primary driver, then the paper's implication that "more data is better" — and that further scaling the dataset would yield further gains — may be misleading. Adding more examples from already well-covered domains (e.g., more algebraic identities similar to those already in the dataset) might yield diminishing or zero returns, while adding examples from underrepresented domains (e.g., complex analysis, graph theory) might yield large returns even with small quantities. The paper provides no guidance on this because it does not analyze the synthetic data's domain composition or the relationship between domain coverage and benchmark performance. A practitioner attempting to replicate the approach with a different informal problem corpus would not know whether to prioritize corpus size or corpus diversity.

The ablation in Table 5 (scaling synthetic data) further complicates the interpretation. The paper describes the dataset size increase as "exponential" (Section 4.3.4), but if smaller subsets are sampled randomly from the full 8 million examples, they would approximately preserve the domain distribution — meaning larger subsets provide more examples per domain, not more domains. In that case, the improvement from larger subsets would indeed reflect a quantity benefit, not just diversity. But the paper does not describe the sampling strategy for Table 5, so this cannot be determined.

What evidence exists in the paper. The quality scoring ablation (Table 3) shows that high-scoring formal statements yield better downstream performance than low-scoring ones — but this is a quality signal within the dataset, not a domain composition analysis. The iterative enhancement ablation (Table 4) shows compounding gains across iterations — but this could be due to improved quality within the same domains rather than expanded domain coverage. The paper provides no table or figure breaking down the synthetic dataset by mathematical domain, no analysis of which domains are represented and in what proportions, and no stratified evaluation on miniF2F showing per-domain improvement.

Mitigation status. Not addressed. The paper does not analyze domain composition, does not provide a domain-stratified evaluation, and does not discuss the domain diversity vs. quantity confound. The conclusion frames future work as "expanding the diversity of mathematical problems addressed" (Section 6), implicitly acknowledging that current domain coverage is limited, but without analyzing how that limitation affects the current results.

7. Implications and Future Directions

How This Work Changes the Landscape

This work fundamentally reframes the neural theorem proving bottleneck from model architecture and search to training data volume, achievable through systematic synthetic generation. Prior to DeepSeek-Prover, the dominant narrative in the field — reinforced by the success of tree search methods like Hypertree Proof Search and Curriculum Learning — was that the core challenge was navigating the vast proof search space. The assumption, rarely stated explicitly but embedded in the architecture of every tactic-by-tactic interactive prover, was that models could not be trusted to generate entire correct proofs in one pass, and that verifier feedback at each step was essential to keep generation on track. DeepSeek-Prover's 46.3% whole-proof accuracy at 64 samples on miniF2F-test — more than doubling GPT-4's 23.0% at the same budget and surpassing Hypertree Proof Search's 41.0% achieved through 64×5000 interactive search steps — forces a reevaluation of this assumption. The model does not merely compete with interactive search; it outperforms it without any verifier feedback during generation, using only the knowledge internalized from 8 million synthetic training examples.

The magnitude of this shift is best characterized as a reframing of the primary bottleneck rather than a paradigm revolution. The paper does not prove that search is obsolete — the FIMO results (5/148 solved, with minimal gains from 100 to 4,096 samples) suggest that for the hardest problems, something beyond current whole-proof generation is needed. But it does demonstrate that for competition-level mathematics (the difficulty tier of miniF2F, which includes AIME and AMC problems), learned proof strategies from large-scale data dominate inference-time search strategies. This is analogous to the shift in machine translation circa 2016: neural models did not render phrase-based statistical systems conceptually obsolete, but they demonstrated that with sufficient training data, end-to-end learned generation could outperform carefully engineered search-and-scoring pipelines. The implication is the same here: research investment should shift from designing more sophisticated proof search algorithms toward designing better data generation pipelines.

The paper also resolves a latent tension in the autoformalization literature. Prior work (Wu et al., 2022; Jiang et al., 2022b; Huang et al., 2024) treated autoformalization as a precision-critical translation task — the goal was to produce formal statements that exactly matched their informal counterparts. This framing implicitly assumed that autoformalization errors were toxic to downstream training, because training on incorrectly formalized theorems would teach the model to prove false statements or use invalid reasoning. The paper inverts this: by pairing autoformalization with a verifier (Lean 4) and a dual-stream proof search that proves negations of incorrect formalizations, autoformalization errors become productive training signal — the proofs of negated false statements teach the model logical discrimination and counterexample construction, which are genuine theorem-proving skills. This reframing converts autoformalization from a quality-critical bottleneck into a throughput-critical component, where the metric of interest is not translation accuracy but the rate at which verified theorem-proof pairs (of either polarity) are generated. This is a conceptual shift with practical consequences: future autoformalization systems should prioritize coverage and diversity over precision, because verification downstream can separate wheat from chaff and even extract value from the chaff.

The work also makes interactive search less attractive as a default architecture for neural theorem provers targeting competition-level mathematics. Whole-proof generation with a fine-tuned 7B model achieves higher accuracy than interactive search with models up to 34B parameters (Llemma 34B achieves 25.8% on miniF2F-test with 1×3200 search steps; DeepSeek-Prover achieves 46.3% at 64 whole-proof samples). If the field's goal is to maximize benchmark performance on problems of this difficulty, the evidence suggests that investing compute in generating and training on synthetic data yields higher returns than investing the same compute in running interactive search at inference time. This does not mean interactive search is valueless — for problems beyond the model's single-pass capability, search may still be necessary — but it does mean that a pure whole-proof generation system should be the strong baseline against which any new search method must justify its additional complexity and cost.

However, the paper also sharpens the known difficulty ceiling for pure data-scaling approaches. The FIMO results (5/148, 3.4%) and the miniF2F saturation curve (30.0% greedy → 46.3% at 64 samples → plateau → 50.0% at 65,536 samples) demonstrate that synthetic data from competition-level problems cannot, by itself, produce a model capable of IMO-level theorem proving at practical success rates. There is a capability gap between the difficulty of problems in the informal training corpus (high-school and undergraduate competition) and the difficulty of FIMO (IMO shortlist) that data scaling alone does not bridge. This establishes a clear boundary condition for the approach: synthetic data from problems at difficulty level D can produce a prover effective at difficulty ≤ D, but does not automatically generalize to difficulty D+1. The implication for the field is that advancing beyond the competition-level ceiling will require either synthetic data at higher difficulty tiers, larger base models that can abstract proof patterns across difficulty levels, or a return to search-based methods for the hardest problems, with whole-proof generation handling everything else.

Follow-Up Research This Work Enables

Cross-model fine-tuning to isolate the contribution of the synthetic dataset from the base model's pretraining. The paper demonstrates that DeepSeekMath-Base 7B + synthetic data fine-tuning yields state-of-the-art performance, but cannot determine whether the 8 million theorem-proof pairs would similarly improve other base models — Llemma 7B, CodeLlama 7B, Mistral 7B, or even a general-purpose model like LLaMA-2 7B. A controlled experiment that fine-tunes each of these models on the same synthetic dataset and evaluates on miniF2F and FIMO would answer several critical questions: (a) does DeepSeekMath-Base's 120B-token mathematical pretraining confer a unique advantage, or is the synthetic data sufficient to teach formal proof generation to any competent base model? (b) do code-specialized models transfer better to Lean 4 (which is both a programming language and a proof system) than general-purpose models? (c) what is the performance ceiling attributable purely to the synthetic data, independent of pretraining? If Llemma 7B achieves comparable performance, the dataset itself is the primary contribution, and the field should focus on scaling and diversifying synthetic data. If only DeepSeekMath-Base responds strongly, then the interaction between mathematical pretraining and formal proof fine-tuning becomes a central research question, with implications for how future base models should be designed.

Domain-stratified evaluation to measure generalization vs. memorization in the synthetic data. The paper reports aggregate performance on miniF2F and FIMO but provides no breakdown by mathematical domain (algebra, number theory, combinatorics, geometry) despite stating that the synthetic data emphasizes algebra and number theory. A domain-stratified evaluation would reveal whether DeepSeek-Prover's gains concentrate in the heavily represented domains (suggesting the model is learning domain-specific proof patterns rather than general theorem-proving skill) or distribute evenly across all miniF2F domains (suggesting the synthetic data teaches transferable reasoning strategies). This experiment would involve: (a) classifying the 244 miniF2F-test problems into domain categories, (b) reporting per-domain accuracy for DeepSeek-Prover at, say, 64 samples, and (c) comparing against the per-domain accuracy of DeepSeekMath-Base and GPT-4 to compute per-domain improvement attributable to synthetic data. If improvement is uniform, the synthetic data approach generalizes, and future work can confidently scale to new domains. If improvement is concentrated in algebra/number theory, future work must explicitly generate synthetic data for underrepresented domains rather than assuming scale alone will suffice.

Synthetic data generation at IMO difficulty to probe the scalability ceiling. The FIMO results (5/148 at 4,096 attempts) indicate a hard capability ceiling that competition-level synthetic data does not breach. A natural follow-up experiment is to apply the exact same pipeline — autoformalization, quality filtering, dual-stream proof search, iterative fine-tuning — to an informal problem corpus drawn from IMO and national olympiad problems rather than high-school and undergraduate competitions. This would test two competing hypotheses: (a) the ceiling is a data difficulty mismatch — IMO problems require proof strategies (non-trivial induction, combinatorial constructions, inequality chains with multiple intermediate lemmas) that are underrepresented in the competition-level corpus, and training on olympiad-level synthetic data would close much of the gap; or (b) the ceiling is a model capacity or architecture limitation — a 7B-parameter model fundamentally cannot internalize the reasoning patterns needed for IMO problems regardless of training data, and scaling to larger models is necessary. If (a), the synthetic data approach generalizes across difficulty tiers and the primary bottleneck is curating high-difficulty informal corpora. If (b), the paper's approach is bounded by model scale, and future investment should shift toward larger base models rather than more synthetic data. A strong version of this experiment would generate 1-5 million olympiad-level theorem-proof pairs (even if the initial autoformalization quality is lower, the iterative pipeline should improve it), fine-tune DeepSeekMath-Base 7B on this data, and evaluate on FIMO. A null result (no improvement over 5/148) would be as informative as a positive one.

Reintroducing interactive search on top of the fine-tuned whole-proof generator. The paper establishes whole-proof generation as a strong baseline but does not test whether the fine-tuned model benefits from inference-time search. A straightforward experiment: take DeepSeek-Prover, allow it to generate proofs interactively (one tactic at a time, with Lean 4 returning proof states between steps), and compare pass@k against pure whole-proof generation at matched inference FLOPs. This would answer whether the model's internalized proof knowledge — acquired from 8 million complete proofs — transfers to the interactive setting where it must generate tactics conditioned on dynamically evolving proof states, or whether the model is brittle and relies on the holistic planning enabled by generating the entire proof in one pass. If interactive search yields substantial gains (e.g., 60%+ on miniF2F-test), the optimal deployment strategy combines synthetic data fine-tuning with lightweight search, and the paper's whole-proof-only framing underestimates the model's capability. If interactive search adds nothing or degrades performance, it would confirm that the model has learned to plan complete proofs and that step-by-step generation disrupts this planning — a strong negative result that would challenge the interactive search paradigm for models with sufficient training data.

Quantitative characterization of the dual-stream proof search efficiency gain. The paper argues that proving negations in parallel accelerates the pipeline by terminating early on unprovable statements, but provides no numbers: what fraction of autoformalized statements are caught by negation-proving vs. the original proof succeeding vs. timing out? What is the distribution of proof attempt counts before termination? A systematic measurement on a representative sample (e.g., 10,000 autoformalized statements with varying difficulty) would characterize the efficiency of the dual-stream approach: the fraction of compute saved vs. single-stream brute force, the correlation between statement correctness and which stream succeeds first, and the false positive/negative rates of the negation-proving filter. This analysis would provide engineering guidance for future pipeline builders and could reveal whether the dual-stream architecture is essential or merely a modest optimization over single-stream search with a timeout. If, for example, 80% of unprovable statements are caught by negation-proving within 8 attempts, the dual-stream approach is a major efficiency win and should be a standard component of synthetic data pipelines; if only 10% are caught, the benefit is marginal and the mechanism should be simplified.

Automated difficulty estimation to reduce wasted compute on unprovable statements. The current pipeline expends proof search budget uniformly across all filtered formal statements, regardless of their likely difficulty or provability. A learned difficulty estimator — a lightweight classifier that takes a formal statement as input and predicts the probability that it will be proved within a given budget — could be trained on the outcomes of the dual-stream search (proved original / proved negation / neither) and used to allocate compute unevenly: easy-looking statements get a small budget, hard-looking statements get a large budget, and statements predicted to be unprovable get zero budget. This is directly analogous to the difficulty estimation approach in the test-time compute scaling paper analyzed earlier, applied to data generation rather than inference. The paper's existing pipeline already produces the necessary training data for such a classifier: for each of the 712,073+ formal statements, we know whether it was proved, disproved, or abandoned, and at what attempt count. A follow-up could train a lightweight model (e.g., fine-tuning a small encoder on these labels) and measure whether difficulty-adaptive budget allocation increases the rate of verified proof generation per GPU-hour compared to uniform allocation. A positive result would make the pipeline substantially more compute-efficient, reducing one of the paper's chief unaddressed limitations (opaque and potentially enormous compute costs).

Practical Applications and Downstream Use Cases

Automated formalization of undergraduate mathematics textbooks and problem sets. The paper's most immediate practical application is in formalizing the kind of mathematics that appears in undergraduate curricula — linear algebra identities, number theory exercises, trigonometric manipulations, basic combinatorics. DeepSeek-Prover's 46.3% whole-proof accuracy at 64 samples on miniF2F (which includes problems of exactly this type) means that for approximately half of such problems, a correct Lean 4 proof can be generated with modest compute (64 forward passes through a 7B model). For an educator preparing formalized problem sets for a proof-assistant-based course, this represents a substantial reduction in manual formalization effort: rather than writing each proof by hand, the instructor provides the informal problem statement, the model autoformalizes it and generates a candidate proof, and the instructor only needs to review (and occasionally correct) the output. The 30.0% greedy accuracy means that even a single sample yields a correct proof for nearly one-third of problems — enough to be practically useful as a first-draft generator. The key enabler is that the model covers the specific difficulty tier and mathematical domains (algebra, number theory) that dominate undergraduate problem sets, making this a targeted rather than speculative application.

Bootstrapping formal mathematics libraries for underrepresented domains. Mathlib, the standard Lean 4 mathematics library, is comprehensive in some areas (basic algebra, linear algebra, topology) but sparse in others — particularly applied mathematics, discrete mathematics, and specialized competition topics. The synthetic data pipeline provides a mechanism for rapidly populating formal libraries in these underrepresented domains: curate an informal problem corpus targeting the desired domain (e.g., 50,000 combinatorics problems from undergraduate exams and competitions), run the autoformalization + proof generation pipeline, and add the verified theorem-proof pairs to mathlib or a domain-specific library. Because the pipeline requires no human annotation — only informal problem statements and a base model capable of autoformalization — the marginal cost of adding a new domain is primarily the cost of curating the informal corpus and the compute for proof generation. The 8 million theorem-proof pairs generated in this work, spanning primarily algebra and number theory, demonstrate the throughput achievable within a focused domain. Extending this to combinatorics, probability, or elementary graph theory would create formal mathematics resources that the small community of human formalizers has not had bandwidth to produce.

Pre-training data for larger neural theorem provers. The 8 million synthetic theorem-proof pairs — all verified correct by Lean 4 — constitute a high-quality, large-scale dataset that could serve as pre-training or intermediate fine-tuning data for larger models targeting formal mathematics. The paper demonstrates effectiveness on a 7B model; the dataset is model-agnostic (it consists of plain Lean 4 code with verification guarantees) and could be incorporated into the training pipeline of models at 34B, 70B, or larger scales. For an organization training a frontier mathematical reasoning model, adding these 8 million examples to the training corpus provides exposure to formal proof syntax and verified reasoning chains that would be extremely sparse in any naturally occurring text corpus — even a mathematics-heavy one. The open-source release of both the dataset and the model enables this: a team training a 34B mathematical model could include the DeepSeek-Prover synthetic data as a domain-specific component of their training mix, potentially improving the larger model's formal proof generation without requiring the larger model to be fine-tuned exclusively on formal data.

Verification-backed code generation for safety-critical mathematical software. While the paper focuses on theorem proving within proof assistants, the underlying capability — generating formally verified mathematical reasoning — has implications for safety-critical software that relies on mathematical correctness guarantees. Examples include cryptographic protocol implementations (where correctness depends on number-theoretic properties), control systems for aerospace or medical devices (where stability proofs depend on real analysis), and financial models (where arbitrage-free pricing depends on stochastic calculus). In each case, the current practice is to implement the mathematics in a conventional programming language and verify correctness through testing — an approach that cannot provide formal guarantees. DeepSeek-Prover-style models, fine-tuned on domain-specific formal verification data, could generate verified implementations alongside their proofs, providing machine-checkable correctness guarantees. The paper's domain restriction to algebra and number theory maps naturally onto cryptographic applications; extending the pipeline to real analysis and probability theory (requiring new informal corpora and possibly larger models) would unlock verification for control theory and financial mathematics.

When to Prefer This Method

The paper positions whole-proof generation with synthetic data fine-tuning against two alternatives — interactive tree search methods (GPT-f, Hypertree Proof Search, ReProver) and general-purpose LLMs used without domain-specific fine-tuning (GPT-4, DeepSeekMath-Base in zero-shot mode) — and the experimental results in Table 1 provide clear guidance on when to prefer each approach based on the available resources and problem characteristics:

• Prefer whole-proof generation with synthetic data fine-tuning (the DeepSeek-Prover approach) when: (1) the target problems fall within the difficulty range of high-school to undergraduate competition mathematics (the miniF2F tier), where the model achieves 46–52% accuracy; (2) the mathematical domains are predominantly algebra and number theory, with some coverage of combinatorics and geometry; (3) inference-time latency is a concern — whole-proof generation requires one forward pass plus one verification check, versus hundreds to thousands of interactive steps for tree search; (4) a modest compute budget is available for synthetic data generation (the 8 million examples were produced through the iterative pipeline described in Section 3, though exact costs are not reported); and (5) the goal is to maximize pass rate on problems the model can solve, not to push the frontier of problem difficulty.

• Prefer interactive tree search when: (1) the target problems are substantially harder than the synthetic training data (e.g., IMO-level or research mathematics), since the FIMO results show DeepSeek-Prover solving only 5/148 problems even with 4,096 samples — tree search may extract additional capability from a model that cannot solve problems in a single pass; (2) the available training data is limited and cannot support large-scale synthetic data generation (tree search methods in Table 1, such as Proof Artifact Co-Training at 24.6% on miniF2F-test with an 837M model, operate with far less training data than 8 million examples); or (3) the model is small (sub-1B parameters), where the interactive feedback from the proof assistant may compensate for the model's limited capacity to plan complete proofs — the 600M Hypertree Proof Search model achieves 41.0%, which is competitive with DeepSeek-Prover's 46.3% despite being 12× smaller, suggesting an efficiency advantage at small scales that the paper's compute-uncontrolled comparison cannot definitively assess.

• Prefer general-purpose LLMs (GPT-4) without domain-specific fine-tuning when: (1) the goal is to quickly prototype formal proofs for a small number of problems without investing in synthetic data generation or model fine-tuning; (2) the problems span diverse mathematical domains not covered by the synthetic data (e.g., topology, abstract algebra), where GPT-4's broad pretraining may provide some capability that a narrowly fine-tuned model lacks; or (3) the user does not have access to the infrastructure for large-scale fine-tuning and dataset generation. However, Table 1 shows GPT-4 achieving only 23.0% on miniF2F-test at 64 samples — less than half of DeepSeek-Prover's 46.3% — so this preference is primarily about minimizing upfront investment, not maximizing accuracy.

These decision boundaries are approximate because the paper does not provide the compute-normalized comparisons that would enable precise tradeoff analysis. The advice to prefer whole-proof generation over tree search at the miniF2F difficulty tier is well-supported by the accuracy numbers in Table 1. The advice to prefer tree search for harder problems is an extrapolation from the FIMO results (where neither approach performs well, but tree search has not been tested at this difficulty tier with a comparably fine-tuned model) and should be treated as a hypothesis rather than a demonstrated fact.