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
TL;DR
Formal theorem proving with LLMs remains challenging and computationally expensive despite progress in natural-language proof generation. Seed-Prover 1.5 combines agentic reinforcement learning with a natural-language-to-Lean sketch workflow, achieving strong results across undergraduate, graduate, and PhD-level benchmarks while retaining limitations on frontier mathematical research.
Problem
LLM-based formal theorem proving remains challenging and computationally expensive, especially for undergraduate-level and more advanced problems, despite progress in natural-language proof generation.
Method
Seed-Prover 1.5 trains a tool-integrated Lean agent with large-scale reinforcement learning and uses a sketch model plus hierarchical test-time workflow to bridge natural-language proofs and Lean.
Results
Seed-Prover 1.5 solves 88% of PutnamBench problems, 80% of Fate-H problems, and 33% of Fate-X problems, including 11 of 12 Putnam 2025 problems within 9 hours.
Takeaways & Limitations
The results indicate that learning from formal interaction experience and high-quality Lean feedback can support efficient formal mathematical reasoning across multiple difficulty levels.
Takeaways & Limitations
The system still faces challenges with PhD-level problems and cannot yet make significant mathematical contributions comparable to human experts.
Abstract
from arXiv · showhide
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
Seed-Prover 1.5 addresses the capability and efficiency gap between natural-language and formal theorem proving by combining agentic reinforcement learning, formal feedback, and natural-language proof decomposition. It reports strong benchmark performance across undergraduate, graduate, and PhD-level problems.
- The work frames formal proving as rigorous and trustworthy while emphasizing its persistent capability and efficiency gap relative to natural-language proving.Lean verification is described as eliminating hallucinations and logical errors in formal proofs.
- Lean provides fully verifiable feedback that supports experience accumulation and large-scale agentic reinforcement learning.The paper presents this environment as a potential advantage over less directly verifiable proving settings.
- A sketch model bridges natural-language proofs and Lean by generating lemma-based sketches that decompose problems into parallel sub-problems.This decomposition supports an efficient test-time scaling workflow.
- Seed-Prover 1.5 trains an agentic prover through large-scale reinforcement learning in an environment integrating Lean and other tools.The agent learns interaction strategies and tool usage for formal theorem proving.
- 88% of Putnam problems, 80% of Fate-H problems, and 33% of Fate-X problems are solved by Seed-Prover 1.5.The system also solved 11 of 12 Putnam 2025 problems within 9 hours.
2 Related Works
Prior LLM theorem provers mainly use step-level or whole-proof interaction with Lean, but both approaches interact inefficiently. Seed-Prover 1.5 instead uses an agent-based prover and a sketch model to balance interaction and bridge natural and formal proofs.
- Step-level provers interact with Lean after each tactic, whereas whole-proof models interact only once after generating complete Lean code.The paper characterizes these as two broad categories of LLM-based theorem provers.
- Both prior interaction paradigms are inefficient because step-level models interact too frequently while whole-proof models interact too sparsely.Seed-Prover 1.5 is presented as using lemma-level interaction to achieve a more balanced approach.
- Seed-Prover 1.5 combines an agent-based Lean prover with rubric reinforcement learning for a sketch model that bridges natural-language proofs and Lean sketches.This distinguishes the approach from Hilbert’s division between a general reasoning model and a specialized Lean model.
3 Approach
The approach combines a tool-integrated Lean agent, reinforcement-learning post-training, a natural-language-to-Lean sketch model, and hierarchical test-time decomposition. Its workflow incrementally verifies lemmas, caches successful results, and recursively refines unresolved sub-goals.
- 3.1 Agentic Prover: The agentic prover incrementally invokes tools, verifies lemmas with Lean, caches compiled lemmas, and reuses them in later reasoning steps.Caching avoids regenerating previously verified code and improves context efficiency.
- 3.1 Agentic Prover: Given a Lean statement, the agent reasons in natural language, searches Mathlib, constructs lemma proofs, and terminates after verification or an interaction budget is exhausted.The configured budget is a maximum sequence length of 64K and 28 tool calls.
- 3.2 Post-training of Agentic Prover: Reinforcement-learning post-training teaches the agent tool-use patterns and interaction strategies in a Lean environment.Training includes direct formal proving, proof-sketch conditioning, and summaries of failed attempts.
- 3.3 Sketch Model: The sketch model uses Lean structural verification and an LLM-as-a-Judge rubric to produce a strict binary reward for lemma-based decomposition quality.Natural-language verification can reject mathematically invalid lemmas before overall sketch evaluation.
- 3.4 Test-Time Workflow: Seed-Prover 1.5 uses a hierarchical test-time workflow to decompose complex proofs and assign sub-goals across specialized agents.The system orchestrates a natural-language prover, sketch model, and agentic Lean prover.
- 3.4 Test-Time Workflow: The workflow recursively converts natural-language proofs into Lean sketches and assigns each unresolved lemma to the agentic prover under a Pass@3 × 3 budget.Disproved lemmas trigger sketch refinement, while unresolved lemmas prompt further decomposition.
4 Experiments
Experiments evaluate Seed-Prover 1.5 across undergraduate, graduate, competition, and frontier-math benchmarks, while tracking training dynamics, adaptive search, and test-time scaling. The system improves formal-proving performance and efficiency, but remains limited on PhD-level and frontier research problems.
- Training Dynamics: RL training accuracy increased from approximately 50% at initialization to nearly 90% after more than 1000 steps.The authors attribute the improvement to curated proof-task data and accurate Lean-based reward signals.
- Training Dynamics: Average function calls fell from approximately 15 to 10 while average sequence length declined from approximately 28k to 17k tokens during RL training.The authors interpret this as more strategic tool use with fewer redundant invocations, while longer-response scoring metrics also improved.
- Adaptive Search Behavior: Fate-H inference averaged approximately 10 search calls per trajectory versus 1–2 on Putnam, while later checkpoints used fewer calls as performance improved.The authors associate this dataset-dependent behavior with Mathlib search needs and faster identification of key lemmas.
- Test-Time Scaling: Increasing test-time compute through search width and depth produced a log-linear increase in PutnamBench solve rate, with most problems solved in the first few hours.A long tail of harder problems emerged as search continued to the 53rd hour.
- Evaluation Results: 87.9% of PutnamBench and 80% of Fate-H problems were solved, with advantages over AlphaProof, Hilbert Prover, and Aleph Prover on PutnamBench.Seed-Prover 1.5 also outperformed Seed-Prover 1.0 across benchmarks while using a reduced compute budget.
- Evaluation Results: 11 of 12 Putnam 2025 problems were solved within 9 hours using a maximum budget of 40 H20-days per problem.The evaluation increased parallel width while capping maximum search depth at 4.
- Limitations: Seed-Prover 1.5 solved selected Erdős problems, but the authors report that these were relatively simple or sometimes simplified by mis-formalization.They state that current systems remain some distance from making mathematical contributions comparable to human experts.
5 Conclusion
Seed-Prover 1.5 performs strongly on competitive mathematics and graduate-level tasks but cannot yet make significant contributions comparable to human experts. The stated limitation is a dependency issue: frontier research requires synthesizing insights across related papers.
- The system performs strongly on competitive mathematics problems and graduate-level mathematical tasks.
- Its main limitation is that it cannot yet make significant mathematical contributions comparable to human experts.
- Frontier mathematical progress requires identifying relevant papers, grounding natural-language proofs in them, and developing scalable formal methods.
A Contributors
The contributor names are sorted alphabetically, and an asterisk marks a member who left Seed.
- The remaining contributors include Chenrui Wei through Thomas Hanwen Zhu, with Fan Yang marked as having left Seed.
- The contributor list contains Jiangjie Chen through Jiacheng Du.
- The contributor list continues from Jinyi Hu through Mingxuan Wang.
B Prompts of Rubric RL and Example of Sketch
The rubric prompts evaluate formal statements and proof sketches for correctness, Lean-specific edge cases, and alignment with an explicit proof strategy. They also reject decompositions that merely restate the goal or hide the main theorem's logical assembly.
- Prompt 1: Atomic Lemma Verification: The evaluation first checks whether a formal statement is mathematically correct and provable, including counterexamples, missing hypotheses, and Lean's total-function junk values.Examples include missing Integrable or Summable assumptions and edge cases such as division by zero, divergent sums, and natural-number subtraction.
- Prompt 1: Atomic Lemma Verification: A statement can be rejected when Lean's default values make an otherwise familiar mathematical claim false.The prompts specifically require checking denominators, infinite sums, and other total-function edge cases before assigning a correct verdict.
- Prompt 2: Proof Strategy Alignment: The proof-strategy evaluator asks whether a sketch is logically sound and actually reduces search complexity, with a fundamentally flawed plan receiving a VETO.A low-scoring PASS may still apply when the plan works but does not significantly simplify the problem.
- Prompt 2: Proof Strategy Alignment: The top-level proof must explicitly combine helper lemmas rather than delegate the entire goal to a wrapper lemma.The rubric vetoes hollow proof bodies because hiding the synthesis step makes the plan's logic impossible to evaluate.
- Prompt 2: Proof Strategy Alignment: Valid top-down decomposition is desirable, but merely restating the hypothesis or entire theorem goal is not a meaningful decomposition.The rubric distinguishes breaking a complex goal into primary logical components from decomposition that adds no simplification.