PaperlayerView exact revision on arXiv

Source-linked AI summary

Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience

Jiangjie Chen, Wenxiang Chen, Jiacheng Du, Jinyi Hu, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Wenlei Shi, Zhihong Wang, Mingxuan Wang, Chenrui Wei, Shufa Wei, Huajian Xin, Fan Yang, Weihao Gao, Zheng Yuan, Tianyang Zhan, Zeyu Zheng, Tianxi Zhou, Thomas Hanwen Zhu

arXiv:2512.17260v1cs.CL

TL;DR

Formal theorem proving with LLMs remains challenging and computationally expensive, especially at undergraduate level and beyond. Seed-Prover 1.5 combines large-scale agentic reinforcement learning with test-time scaling and reports state-of-the-art performance across benchmarks, solving 88% of Putnam, 80% of Fate-H, and 33% of Fate-X problems.

  • Problem

    Formal theorem proving in Lean remains less capable and efficient than natural-language proving, while large-scale RL for agentic provers remains underexplored.

    Source: §1 · p. 2

  • Method

    The authors train an agentic Lean prover through large-scale RL to learn interaction strategies and tool use, then use a sketch model and test-time workflow to bridge natural-language proofs and formalization.

    Source: §1 · p. 2

  • Results

    Seed-Prover 1.5 achieves state-of-the-art performance across key benchmarks at moderate compute, solving 88% of Putnam, 80% of Fate-H, and 33% of Fate-X problems.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The reported results show LLM-based formal proving has narrowed the capability and efficiency gap with natural-language reasoning at undergraduate and graduate levels.

    Source: §1 · p. 2

    The authors report that the system remains some distance from advancing frontier open mathematical problems, and some observed solutions were trivial or simplified versions caused by mis-formalization.

    Source: §4.2 · p. 9

Abstract

from arXiv · show

Large language models have recently made significant progress to generate rigorous mathematical proofs. In contrast, utilizing LLMs for theorem proving in formal languages (such as Lean) remains challenging and computationally expensive, particularly when addressing problems at the undergraduate level and beyond. In this work, we present \textbf{Seed-Prover 1.5}, a formal theorem-proving model trained via large-scale agentic reinforcement learning, alongside an efficient test-time scaling (TTS) workflow. Through extensive interactions with Lean and other tools, the model continuously accumulates experience during the RL process, substantially enhancing the capability and efficiency of formal theorem proving. Furthermore, leveraging recent advancements in natural language proving, our TTS workflow efficiently bridges the gap between natural and formal languages. Compared to state-of-the-art methods, Seed-Prover 1.5 achieves superior performance with a smaller compute budget. It solves \textbf{88\% of PutnamBench} (undergraduate-level), \textbf{80\% of Fate-H} (graduate-level), and \textbf{33\% of Fate-X} (PhD-level) problems. Notably, using our system, we solved \textbf{11 out of 12 problems} from Putnam 2025 within 9 hours. Our findings suggest that scaling learning from experience, driven by high-quality formal feedback, holds immense potential for the future of formal mathematical reasoning.

1 Introduction

The introduction argues that Lean’s verifiable environment enables experience-driven agentic reinforcement learning, and presents Seed-Prover 1.5’s prover-and-sketch workflow. The system reports strong results across undergraduate-, graduate-, and PhD-level benchmarks.

Introduction

  • Lean verification avoids hallucinations and logical errors, but formal proving still faces a substantial capability and efficiency gap relative to natural-language proving.The introduction contrasts DeepSeek-Math-V2’s near-perfect Putnam 2024 scores with AlphaProof solving 56% of the full Putnam benchmark despite approximately 500 TPU-days per problem.Source: §1 · p. 2
  • Large-scale RL trains an agentic prover to learn interaction strategies and tool use in Lean’s verifiable environment, where it can explore and receive ground-truth feedback.The agent dynamically adjusts interaction granularity and uses auxiliary tools, unlike step-level or whole-proof approaches.Source: §1 · p. 2
  • A Rubric-RL-trained sketch model generates lemma-based Lean sketches that decompose problems into parallel subproblems, supporting an efficient test-time scaling workflow.The sketches bridge natural-language proofs and formalization.Source: §1 · p. 2
  • Seed-Prover 1.5 solves 88% of Putnam, 80% of Fate-H, and 33% of Fate-X problems, and proves 11 of 12 Putnam 2025 problems within 9 hours.The paper presents these results as state-of-the-art performance across key benchmarks and evidence that formal proving has narrowed the gap with natural-language reasoning at undergraduate and graduate levels.Source: §1 · p. 2

2 Related Works

Prior Lean-based LLM provers use step-level tactics or whole-proof generation, interacting with Lean either too frequently or too sparsely. Seed-Prover 1.5 instead uses an agent-based approach that interacts through lemmas and trains a sketch model with rubric reinforcement learning to bridge natural-language proofs and Lean sketches.

2 Related Works

  • Seed-Prover 1.5 uses an agent-based prover that interacts with Lean through lemmas, balancing the frequent interactions of step-level provers and sparse interactions of whole-proof models.Step-level models generate one tactic per proof state, while whole-proof models generate complete Lean code and interact only once.Source: §2 · p. 2
  • LLM-based Lean provers broadly use step-level interaction [1, 8, 25, 27, 28] or whole-proof generation [3, 9, 12, 13, 18, 19, 23, 26, 33].Several systems integrating Lean 4 with LLMs have achieved IMO-level mathematical proving capabilities [1] [3].Source: §2 · p. 2
  • Unlike Hilbert [22], which pairs a general reasoning model for informal proofs with a specialized Lean model for verification, Seed-Prover 1.5 uses rubric reinforcement learning [6] for a sketch model and trains an agent-based Lean prover.Hilbert achieves strong performance on PutnamBench; Seed-Prover 1.5’s sketch model bridges natural-language proofs and Lean sketches.Source: §2 · pp. 2–3

3 Approach

Seed-Prover 1.5 combines an incrementally tool-using Lean prover, reinforcement-learning post-training, and a sketch model with a hierarchical test-time workflow. The workflow connects natural-language proofs to Lean sketches and verified subproofs.

3.1 Agentic Prover

  • Unlike whole-proof generation [19], the prover constructs proofs lemma by lemma, caching verified lemmas to reduce context overhead and focus on immediate sub-goals.This supports lemma-style proofs [3] and flexible inference strategies such as pruning irrelevant steps or backtracking to a chosen point.Source: §3.1 · p. 3
  • The agent uses LooKeng [3] for Lean feedback, embedding-based Mathlib retrieval fixed to v4.22.0, and Python execution for computational checks.It accepts a Lean statement with optional natural-language proof or instructions, permits multiple tool calls per turn, and uses a 64K-token maximum sequence length and 28-call limit in experiments.Source: §3.1 · pp. 3–4

3.2 Post-training of Agentic Prover

  • Seed-Prover 1.0 [3] is post-trained as a Lean tool-use agent through synthetic-data SFT, then RL on formal statements, proof sketches, or summaries of failed attempts.RL data mixes public datasets [2] [16] [23] [29] and formalized textbooks, filters examples by SFT difficulty, and rewards proofs verified by Lean (+1) while assigning −1 otherwise; training uses VAPO [31] and tool-integrated RL following ReTool [4].Source: §3.2 · p. 4

3.3 Sketch Model

  • The sketch model converts formal statements and natural-language proofs into lemma-style Lean sketches that split propositions into independent sub-goals.It is trained with VAPO [31] using Lean structural verification and natural-language lemma checking, plus an LLM judge assessing alignment, granularity, difficulty reduction, and Lean junk value.Source: §3.3 · p. 5

3.4 Test-Time Workflow

  • The test-time workflow decomposes complex Lean proofs through three agents: a natural-language prover, a sketch model, and an agentic Lean prover that verifies lemmas.For unsolved lemmas, the system attempts proof or disproof, recursively decomposes failures, and refines sketches when a lemma is disproved; it stops when all leaves are proved or maximum search depth is reached.Source: §3.4 · p. 5

4 Experiments

Seed-Prover 1.5 combines an agentic prover trained through reinforcement learning with a test-time workflow, evaluated on competitions and benchmarks spanning undergraduate to frontier mathematics. The experiments report strong undergraduate- and graduate-level results while identifying remaining limits on very long-context reasoning and frontier problems.

4 Experiments

  • Evaluations covered PutnamBench, FATE [10], CombiBench [14], IMO and Putnam 2025, and a curated Erdős problem subset under Lean v4.22.0.The authors flag significant formalization issues in CombiBench and report its performance for reference; the Erdős subset excluded problems identified as mis-formalized.Source: §4 · pp. 5–6

4.1 Scaling Behavior of the Agentic Prover Training

  • Training accuracy rose from approximately 50% to nearly 90% after more than 1,000 RL steps, while average function calls fell from about 15 to 10.Average sequence length also fell from approximately 28k to 17k tokens, even as long-response scoring improved; negative scores persisted for 32K–64K responses.Source: §4.1 · p. 6, Figure 3 · p. 6, Figure 4 · p. 7
  • Fate-H inference averaged approximately 10 search calls per trajectory versus 1–2 on Putnam, and later checkpoints used fewer calls while performance improved.The authors interpret the trend as adaptation to Mathlib-heavy tasks and internalization of useful search results.Source: §4.1 · p. 7, Figure 5 · p. 8

4.2 Evaluation and Scaling Behavior of the Test-Time Workflow

  • Increasing search width and depth produced a log-linear rise in PutnamBench solve rate, with most problems solved in the first few hours and harder cases appearing through hour 53.The workflow starts with search depth 4 and restarts unresolved searches after adding proven lemmas, extending the maximum depth to 8.Source: §4.2 · p. 8, Figure 6 · p. 8
  • 87.9% on PutnamBench and 80% on Fate-H; Seed-Prover 1.5 outperforms prior methods, including Seed-Prover 1.0, with reduced compute.The system still struggles with PhD-level problems and beyond, partly because of problem complexity and limited Mathlib support.Source: Table 2 · p. 9, §4.2 · p. 9
  • 11 of 12 Putnam 2025 problems were solved within 9 hours, while Seed-Prover 1.5 matched Seed-Prover 1.0’s 5-of-6 IMO 2025 solve rate at comparable-to-Medium compute.The IMO setting used 20 H20-days per problem, with a shorter runtime than Seed-Prover 1.0 Heavy; the Putnam setting allowed up to 40 H20-days per problem.Source: Table 4 · p. 9, §4.2 · p. 9, Table 3 · p. 9
  • Seed-Prover 1.5 solved 15 listed Erdős problems, but the authors caution that these were relatively simple or sometimes trivialized by mis-formalization.They conclude that current natural- and formal-language systems remain some distance from advancing research on frontier open problems.Source: §4.2 · p. 9

5 Conclusion

Seed-Prover 1.5 pairs an agentic Lean prover with a sketch model that bridges natural-language proofs and formal Lean code, and shows strong performance on competitive mathematics problems. The conclusion identifies reliance on prior research as a barrier to human-comparable mathematical contributions and outlines challenges for formal mathematical research.

5 Conclusion

  • Seed-Prover 1.5 combines a high-performance agentic Lean prover with a sketch model bridging natural-language proofs and formal Lean code.Source: §5 · p. 10
  • Despite strong performance on Putnam and graduate-level FATE tasks, the system cannot yet make mathematical contributions comparable to human experts because frontier research depends on synthesizing prior work.Source: §5 · p. 10
  • Progress requires identifying influential papers, proving claims in natural language grounded in them, and scaling formalization of papers and their derived results.Source: §5 · p. 10
  • Solving these challenges could enable large-scale generation of formal mathematical research and contribute to resolving some open mathematical conjectures.Source: §5 · p. 10

Appendix · B Prompts of Rubric RL and Example of Sketch

The appendix documents rubric-based evaluation of formal statements and proof sketches, including checks for Lean-specific edge cases and the soundness and usefulness of proof strategies. It specifies scoring and output conventions and illustrates them with an example sketch and placeholder Lean and natural-language proof inputs.

Prompt 1: Atomic Lemma Verification

  • The atomic-verification prompt treats each formal statement as independent, using the sketch only to resolve definitions and seeking a proof or counterexample rather than trusting listed lemmas.It classifies false statements, missing hypotheses, logical gaps, and failures caused by Lean’s total-function behavior as incorrect.Source: B Prompts of Rubric RL and Example of… · pp. 14–15
  • The verifier checks for missing `Integrable` or `Summable` hypotheses and treats failures caused by Lean’s junk values as evidence that a statement is incorrect.The prompt also calls for checking edge cases such as zero denominators and applying necessary preconditions described in documentation.Source: B Prompts of Rubric RL and Example of… · pp. 14–16

Prompt 2: Proof Strategy Alignment

  • The strategy evaluator uses mandatory foundational checks and vetoes sketches with fatal misalignment between the proposed strategy and the natural-language proof.It also validates every helper lemma before proceeding to scoring.Source: B Prompts of Rubric RL and Example of… · pp. 16–17
  • A sketch must show how its lemmas combine to prove the theorem; delegating that assembly to an opaque wrapper lemma is vetoed, while transparent constructors can pass.The main proof should expose the reasoning rather than hide it in a wrapper with the same goal as the theorem.Source: B Prompts of Rubric RL and Example of… · pp. 17–18
  • Helper lemmas must be true, self-contained, and substantively useful; trivial restatements are invalid, but short library calls and top-down decomposition are not automatically trivial.The prompt also flags lemmas that fail because of Lean junk values.Source: B Prompts of Rubric RL and Example of… · p. 18
  • The scoring rubric rates structural alignment and lemma value at 50% each, distinguishing basic strategic decomposition from deeper search-simplifying plans and high-value self-contained lemmas.Higher-value lemmas isolate concrete solvable subproblems and capture steps from the natural-language proof.Source: B Prompts of Rubric RL and Example of… · pp. 18–19

B Prompts of Rubric RL and Example of Sketch

  • For PASSED sketches, the final score is the rounded weighted alignment/value score multiplied by the fraction of valid proposed lemmas used; VETOED sketches score -10.0.The weighted score uses alignment × 0.4 and value × 0.6; utilization is used lemmas divided by valid proposed lemmas.Source: B Prompts of Rubric RL and Example of… · p. 19
  • The required JSON output conditionally includes veto reasons and invalid-lemma diagnostics, or a passing sketch’s strategy, ideal lemmas, alignment/value/utilization justifications, and scores.The decomposition rubric, justification, and score fields are included only when the evaluation status is PASSED.Source: B Prompts of Rubric RL and Example of… · p. 19
  • Figure 7 shows an example sketch generated by Seed-Prover 1.5; the supplied Lean-entry template includes a Formal Statement field and a Natural Language Proof placeholder.Source: B Prompts of Rubric RL and Example of… · p. 20, Figure 7 · p. 21

Related papers

Loading 2512.17260v1…