Summary (Overview)

• Core contribution: Introduces daVinci-Prover, a family of formal theorem-proving models trained on a novel agent-native mid-training corpus (33.7B tokens) that combines mathematical skill priors with environment-native agent trajectories, plus a lightweight prover harness for collecting high-quality SFT data.
• Key finding: Mid-training improves Qwen3-8B pass@1 by an average of 13.7 points over the matched Base + SFT baseline across MiniF2F, FATE-M, and ProofNet, with consistent gains on Qwen3.5-9B and Qwen3.5-35B-A3B models.
• Harness design: The daVinci-Prover harness enables iterative edit–check–revise loops with Lean4, supporting 7 tools, isolated workspaces, and verifier-grounded feedback; it collects ~36K high-quality agent trajectories for SFT.
• Data ablation: Agent-native trajectories ($\mathcal{D}_{agent}$, 8.4B tokens) yield larger gains than skill-prior data ($\mathcal{D}_{skill}$, 25.3B tokens) alone, but the two are complementary—combining them gives the best performance.
• Memory compaction: A model-free trajectory compression method yields near-saturating MiniF2F performance (97.1 pass@1) and dramatic gains on FATE-H (42.0 for 35B model vs. 16.3 without compaction).

---

Introduction and Theoretical Foundation

Formal theorem proving converts mathematical statements and proofs into machine-checkable computational objects. Lean proof assistants offer an attractive interface for LLMs because they combine mathematical reasoning trajectories with verifiable feedback. The paper identifies three paradigms of LLM-based provers:

1. Whole-proof generation: Complete proofs in a single pass (e.g., DeepSeek-Prover, Goedel Prover).
2. Agentic proving: Model interacts with an executable environment, inspects workspaces, queries libraries, runs Lean, interprets verifier feedback, and iteratively revises proofs.
3. Orchestrated systems: Multiple components coordinated in structured workflows (e.g., Seed-Prover 1.5, Hilbert).

The authors argue that existing formal-reasoning corpora are dominated by whole-proof trajectories, which fail to expose essential proving behaviors such as:

• Decomposing goals into sub-theorems
• Exploring alternative proof steps
• Verifying intermediate reasoning
• Localizing and repairing failures

Key theoretical insight: These capabilities should be injected into mid-training data as reusable mathematical skill priors (not left to post-training). Additionally, agentic provers require agent-native trajectories that capture authentic interactions with Lean—including proof states, verifier feedback, and failed attempts—to reduce the distribution gap between static training and interactive inference.

---

Methodology

3.1 Theorem-Proving Skill Priors ($\mathcal{D}_{skill}$)

Four types of trajectories are constructed:

(a) Decomposition and Assembly Trajectories: A teacher LLM receives a Lean theorem + verified reference proof and generates:

• A natural-language proof plan
• Auxiliary lemmas with dependency information
• A complete assembled Lean proof

(b) Verified Subgoal Search Data: Replaying verified proofs to extract intermediate states, then:

• A proposal model generates diverse tactics
• Tactics are combined with reference tactics, anonymized, shuffled, and executed independently
• Retain successful closures, accepted open states, and Lean errors (exclude timeouts)

(c) Revision Trajectories: Structured diagnosis with four fields:

• location: affected lemma/proof step
• symptom: observed failure
• cause: underlying issue
• fix: targeted correction

(d) Informal Reasoning and Verification Trajectories: From Nemotron-Math-Proofs-v2, covering proof generation with self-evaluation, proof verification, and meta-verification.

3.2 daVinci-Prover Harness

The harness formulates proving as an iterative edit–check–revise loop:

• Input theorem copied into scratch/solution.lean
• 7 tools available (edit candidates, inspect files, retrieve Lean declarations, run focused checks)
• Writable scratch/ directory for proof candidates; read-only target/ for Lean/Mathlib project
• Every edit triggers verification; draft checks expose local goals; placeholder-free candidates undergo strict verification
• Episode terminates only when a candidate passes strict Lean verification AND declaration/type match the original theorem

3.3 Final Dataset: daVinci-Prover 33.7B Collection

Data sources: NuminaMath-LEAN, AoPS, Lean Workbook, Goedel LM/SFT dataset v2, OProofs. Contamination filtering removes 0.03427% of tokens overlapping with evaluation benchmarks.

Data replay: Parent examples (logical trajectories before 32K chunking) are assigned replay budgets; high-quality parents selected with source-specific scores.

Corpus composition:

4 Supervised Fine-Tuning

• Data source: Harness rollouts on Goedel-LM/RL dataset V2 (~99K problems), limited to 30 turns / 200 tool calls, collected with DeepSeek-V4-Flash-0731.
• ~36K high-quality trajectories spanning algebra, number theory, geometry, analysis, combinatorics, topology, probability, linear algebra, abstract algebra, logic.
• Filtering: remove low-quality trajectories (excessive repetition, unnecessary tool calls, <5 turns), retain only those fitting 144K-token context.

---

Empirical Validation / Results

Benchmark Performance (pass@8, daVinci-Prover harness)

Harness Effectiveness (pass@1, 3 runs)

Retrieval tool consistently improves performance, especially on harder benchmarks (FATE-H, Putnam).

Data Component Ablation (Qwen3.5-9B)

Comparison with Existing Corpora (Qwen3-8B)

Memory Compaction Effect (pass@1, 3 runs)

Other Key Findings

• Scaling: Performance follows an approximately log-linear trend with mid-training data volume; most gains achieved within first 15B tokens (3.96 and 11.11 points over base on MiniF2F and FATE-M).
• Training dynamics: Mid-trained checkpoints start SFT with lower loss and remain better aligned; after one epoch, mid-training improves avg@5 by 5.33 (9B) and 5.08 (35B) points, matching base model's epoch-5 pass@5.
• Agent behavior: Mid-trained models show earlier file construction, more auxiliary-check passing (11.8%→12.7% at 9B; 12.6%→13.4% at 35B), and more decomposition on hard problems.

---

Theoretical and Practical Implications

1. Distribution alignment matters: Agent-native trajectories ($\mathcal{D}_{agent}$) provide larger gains per token than skill priors ($\mathcal{D}_{skill}$) because they bridge the gap between static next-token training and interactive proving—models learn the same interaction primitives encountered at inference time.

2. Complementarity of supervision: Skill priors (decomposition, search, diagnosis, self-verification) and agent-native trajectories are not substitutable—combining them consistently outperforms either alone. Effective proving requires both knowing how to reason about a proof and knowing how to realize that reasoning through environment interaction.

3. Mid-training as foundation: Mid-training provides a stronger initialization for downstream SFT, enabling faster adaptation and better final performance. The 9B midtrain model even surpasses the 35B-A3B base model on MiniF2F, suggesting gains come from mid-training rather than model scale.

4. Context management is critical: Memory compaction dramatically improves long-horizon proving (FATE-H: 16.7→28.0 for 9B; 16.3→42.0 for 35B), suggesting that effective context management can better expose the capacity of larger models.

5. Data composition > data scale: Our 33B-token corpus outperforms Oprover's 65B-token corpus, demonstrating that targeted composition (skill priors + agent trajectories) is more effective than sheer volume.

---

Conclusion

The paper introduces daVinci-Prover, combining agent-native mid-training with verifier-grounded supervised fine-tuning for interactive theorem proving. Key takeaways:

• A 33.7B-token mid-training corpus covering decomposition, search, self-verification, revision, and environment-native agent trajectories provides a strong foundation for theorem-proving agents.
• The lightweight daVinci-Prover harness effectively collects ~36K high-quality agent trajectories that transfer proving behavior to smaller models.
• Mid-training consistently improves performance over SFT-only baselines across multiple model families and benchmarks, with ablations confirming the complementary roles of mathematical skill priors and agent-native trajectories.
• Memory compaction enables near-saturating MiniF2F performance and substantial gains on challenging benchmarks.

Future directions implied by the work include: further scaling mid-training data, exploring reinforcement learning on top of the mid-trained initialization, and extending the approach to other proof assistants or interactive reasoning domains. All data, models, harness, and training infrastructure will be open-sourced for reproducibility.