Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
Seed-Prover 1.5 combines agentic RL and test-time scaling, solving 87.9% of PutnamBench.
Key Findings
Methodology
The system combines a natural-language prover, a Sketch Model, and an Agentic Lean Prover. The latter interacts with Lean, Mathlib semantic search, and Python, receiving compiler-based rewards. Training uses SFT, VAPO-style tool-integrated RL, and self-summarization. At inference, lemma-style sketches recursively decompose a theorem, while verified lemmas are cached and reused.
Key Results
- Under Lean v4.22.0, the full system solves 87.9% of PutnamBench, 80% of Fate-H, and 33% of Fate-X. The agentic prover alone reaches 359/660, 57/100, and 10/100 under Pass@8×8.
- Compared with Seed-Prover 1.0's 331/660, 35/100, and 9/100, version 1.5 improves substantially with less compute. RL training accuracy rises from roughly 50% to nearly 90%; average calls fall from about 15 to 10 and sequence length from 28K to 17K tokens.
- Test-time scaling produces approximately log-linear gains. The complete workflow solves 11 of 12 Putnam 2025 problems within nine hours, demonstrating the value of natural-language decomposition plus formal verification.
Significance
The work shows that formal verification can serve not only as a final checker but also as a high-quality learning environment for large-scale reinforcement learning. Lean eliminates many hallucinations and logical gaps, allowing models to explore, cache verified lemmas, and learn tool-use policies. The results narrow the capability gap between natural-language and formal proving, with implications for trustworthy mathematical software, education, and machine-assisted research.
Technical Contribution
The main contribution is a lemma-level interaction paradigm. It is less wasteful than tactic-by-tactic interaction and more controllable than whole-proof generation. LooKeng supplies structured Lean feedback; Mathlib v4.22.0 semantic retrieval and Python extend the toolset; verified lemmas are cached. The Sketch Model uses VAPO, Lean structural checks, and Rubric-based semantic scoring to bridge natural-language arguments and formal subgoals.
Novelty
The novelty lies in the closed loop of experiential learning, formal feedback, and test-time decomposition rather than in model scale alone. Unlike AlphaProof-like step-oriented systems or monolithic generators, the prover dynamically changes interaction granularity and turns natural-language reasoning into a recursively verifiable lemma tree. This is a systematic agentic-RL and TTS design centered on formal feedback.
Limitations
- Performance drops to 33% on Fate-X, reflecting limits in mathematical complexity, long-horizon reasoning, and Mathlib coverage.
- CombiBench contains substantial formalization problems, and erroneous Erdős instances were removed, so cross-benchmark comparisons require caution.
- Negative scores remain for 32K–64K responses; test-time searches can extend to 53 hours, leaving significant computational cost.
Future Work
Future work should iteratively collect more experience from the RL-trained prover, improve long-context planning, error pruning, and search scheduling, and expand Mathlib coverage. Better natural-language verification, parallel subgoal solving, adaptive budgets, and cleaner benchmarks may be necessary to reach PhD-level mathematics and frontier conjectures.
AI Executive Summary
Formal theorem proving asks an AI system to produce Lean code that a kernel can verify, rather than merely plausible prose. Existing step-level systems interact too frequently, while whole-proof generators struggle with long programs and debugging. AlphaProof, for example, solved about 56% of the full Putnam benchmark at an extremely high reported cost. Seed-Prover 1.5 targets this capability-efficiency-reliability trade-off.
The system has three components: a natural-language prover, a Sketch Model, and an Agentic Lean Prover. The first writes a lemma-oriented argument; the second translates it into a Lean sketch with auxiliary lemmas; the third verifies each component using LooKeng, Mathlib semantic search, and Python. Training combines SFT with VAPO-based tool-integrated RL, rewarding successful compilation with +1 and failure with −1. Verified lemmas are cached, while failed or disproved subgoals can be recursively decomposed at test time.
On Lean v4.22.0, the workflow solves 87.9% of PutnamBench, 80% of Fate-H, and 33% of Fate-X. It also solves 11 of 12 Putnam 2025 problems within nine hours. RL raises training accuracy from roughly 50% to nearly 90%, while reducing average tool calls from about 15 to 10 and sequence length from approximately 28K to 17K tokens. The broader lesson is that formal feedback can teach models how to reason and use tools, not merely check answers. Yet PhD-level difficulty, long contexts, Mathlib gaps, and high search costs remain substantial obstacles.
Deep Analysis
Background
Lean enables machine-checked mathematics and suppresses many hallucinations in natural-language proofs. DeepSeek-Math-V2 performs near-perfectly on Putnam 2024, whereas AlphaProof solved only 56% of the easier full Putnam benchmark, exposing a formalization tax. Existing systems largely use step-level tactic interaction or whole-proof generation: the former over-calls Lean, while the latter is difficult to repair.
Core Problem
The goal is to generate compilable Lean proofs from undergraduate through PhD-level mathematics while controlling context, tool calls, and compute. Bottlenecks include discovering Mathlib lemmas, planning thousands of lines of code, handling long horizons, and translating informal arguments into formal syntax. A single interaction granularity cannot jointly optimize local feedback, global structure, and efficiency.
Innovation
- �� The Agentic Prover uses lemmas as interaction units and dynamically calls Lean, Mathlib search, and Python.
- �� RL uses compiler verification as an exact reward for tool-use and recovery behavior.
- �� The Sketch Model converts natural-language proofs into lemma trees using VAPO, Lean structural scoring, and Rubric semantic scoring.
- �� Test-time inference performs recursive decomposition, caching, and Pass@3×3 search, connecting informal reasoning to formal verification.
Methodology
- �� Input: a Lean statement with optional natural-language guidance.
- �� Cold start: SFT from Seed-Prover 1.0 teaches the required tool-call format.
- �� RL: a VAPO-style clipped objective optimizes multi-turn trajectories; verified proofs receive +1 and failures −1.
- �� Tools: LooKeng for compilation, embedding retrieval over fixed Mathlib v4.22.0, and Python execution.
- �� Sketching: the natural-language prover proposes an argument; the Sketch Model generates at least three auxiliary lemmas and a main body.
- �� Search: the Agentic Prover proves leaf lemmas, caches successes, recursively decomposes failures, and stops after completion or a depth limit.
Experiments
Benchmarks include 660 PutnamBench problems, 100 Fate-H problems, 100 Fate-X problems, CombiBench, IMO and Putnam 2025, and selected Erdős problems. Experiments use Lean v4.22.0, a 64K-token maximum sequence length, and up to 28 tool calls. Putnam-200 tracks RL progress. Baselines include Seed-Prover 1.0, AlphaProof, Hilbert Prover, Aleph Prover, and Goedel-Prover-V2-32B. The study also varies RL checkpoints, search depth, width, and compute.
Results
The full system reaches 87.9% on PutnamBench, 80% on Fate-H, and 33% on Fate-X; the agentic-only variant reaches 359/660, 57/100, and 10/100. Seed-Prover 1.0 reaches 331/660, 35/100, and 9/100, so 1.5 improves both accuracy and efficiency. RL accuracy approaches 90%, while calls decline from about 15 to 10. More search width and depth yield near log-linear gains, but difficult instances may take up to 53 hours.
Applications
Potential uses include filling Lean libraries, formalizing textbook and competition problems, proposing auxiliary lemmas, and exploring conjectures with machine-checkable outputs. Deployment requires a stable Lean environment, a fixed Mathlib version, substantial accelerator budget, and expert review. In education, natural-language and formal proofs could be displayed together to teach both intuition and rigor.
Limitations & Outlook
The method remains constrained by Mathlib coverage and formalization quality; 33% on Fate-X is not general PhD-level competence. Long 32K–64K trajectories still fail, and recursive search can require up to 53 hours. The paper does not fully isolate the independent effects of the natural-language prover, Sketch Model, caching, and tools. Future work should improve long-horizon planning, parallelism, automatic error pruning, and benchmark standardization.
Plain Language Accessible to non-experts
Imagine building a bridge. One traditional approach asks an inspector to approve every brick immediately; this is safe but painfully slow. Another draws and builds the entire bridge before inspection; when one beam is wrong, the whole structure is hard to repair. Seed-Prover 1.5 takes a middle path. An explainer first describes the construction plan, a designer divides it into piers, beams, and road sections, and a very strict inspector checks each part.
If one component fails, the system does not rebuild everything. It breaks that component into smaller jobs, searches a library for useful instructions, and may run a small experiment. Completed parts are stored and reused. During training, passing inspection earns a reward and failure receives a penalty, so the builder gradually learns when to search, test, summarize, or stop.
The outcome is impressive: roughly 88% of 660 undergraduate Putnam problems, 80% of graduate-level Fate-H problems, and 33% of PhD-level Fate-X problems. It solved 11 of 12 Putnam 2025 problems in nine hours. The bridge builder is still expensive and struggles with unfamiliar materials, but the work shows that strict checking can also teach an AI how to work more intelligently.
ELI14 Explained like you're 14
Think of a super-hard puzzle game where saying “I think this is right” earns nothing. You must submit every move to a strict referee, and one illegal move means the plan fails. Lean is that referee, and a mathematical proof is the game code you want to get accepted.
Seed-Prover 1.5 is like a team of gaming friends. One teammate explains the strategy in normal language, another chops it into smaller missions, and the Lean teammate checks each mission. If a mission is too hard, it gets split again. If it is solved, the team saves it in its inventory instead of repeating it. The team can also search a math library and run Python experiments.
During training, a completed proof earns one point and a failed attempt loses one. After many games, the model learns when to search, when to test code, and when to summarize a failed attempt. Its training success rises from about 50% to almost 90%, while it uses fewer tool actions.
The scorecard is wild: about 88% on undergraduate Putnam problems, 80% on graduate-level Fate-H, and 33% on PhD-level Fate-X. It solved 11 of 12 Putnam 2025 problems in nine hours! But it still gets stuck on giant proofs, missing library facts, and very advanced math. It is a powerful teammate—not an unbeatable final boss.
Glossary
Agentic Reinforcement Learning
A model learns policies through multi-turn actions, tool feedback, and rewards rather than one-shot generation. Here, the reward is determined by whether Lean successfully compiles the proof.
Used to train the Agentic Lean Prover.
Lean
A proof assistant and executable formal logic system. Its kernel accepts a theorem only after checking the formal proof.
Verifies each lemma and the final theorem.
VAPO
A policy-optimization method that uses advantage estimates and clipped probability ratios. The paper adapts it to trajectories containing tool calls and responses.
Used for RL training of both the prover and sketch model.
Lemma-style Lean sketch
An intermediate representation that decomposes a theorem into auxiliary lemmas and a main proof structure. Some components may initially remain unproved and are filled later.
Generated by the Sketch Model for recursive solving.
Test-time scaling
Increasing inference-time search width, depth, or computation to improve solve rates. The paper observes approximately log-linear gains on PutnamBench.
Drives the Seed-Prover 1.5 workflow.
Mathlib semantic search
Retrieval of relevant theorems, definitions, and lemmas by mathematical meaning rather than only by names. It helps discover unfamiliar library interfaces.
A central auxiliary tool for the Agentic Prover.
Open Questions Unanswered questions from this research
- 1 How can the model remain reliable over 32K–64K or longer trajectories? Negative scores persist, suggesting a need for better memory compression, proof-state abstraction, and long-horizon credit assignment.
- 2 Fate-X failures may reflect mathematics, formalization, or Mathlib coverage, but these causes are not cleanly separated. Fine-grained failure labels and standardized benchmarks are needed.
- 3 How to reduce searches that can last up to 53 hours without sacrificing verification remains a major barrier to deployment in real research workflows.
Applications
Immediate Applications
Formalizing textbooks and problem sets
Teachers and library maintainers can provide a theorem statement and natural-language proof, then use the system to generate lemma sketches and verify them. Correct formalization and a fixed Mathlib version are prerequisites; outputs remain candidate code requiring review.
Research proof assistance
Researchers can request proof decomposition, Mathlib lemma retrieval, Python checks, and Lean verification. The system can reduce mechanical formalization time, but experts must still inspect mathematical assumptions and the final proof structure.
Long-term Vision
Trustworthy AI mathematics partner
With broader Mathlib coverage and cheaper search, the system could support research theorems, conjecture exploration, and machine-checked knowledge bases. Creative PhD-level reasoning, benchmark quality, and interpretable long-term planning remain the main obstacles.
Abstract
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.