arxiv-2512-17260 SRC-0341 · paper

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

Created: 2025-12-19 · Ingested: 2026-09-19

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 accumulat

In brief

An agentic Lean prover that interacts lemma-by-lemma, with tool access to Mathlib search and Python, beats both step-level and whole-proof provers while using less compute, and agentic RL makes it cheaper rather than more expensive per proof.

Seed-Prover 1.5 from ByteDance Seed combines 3 components: a natural-language prover (from Doubao-Seed-1.6), a sketch model trained with rubric RL to turn NL proofs into lemma-style Lean sketches with sorry placeholders, and the RL-trained agentic prover that discharges each lemma. Evaluation covers PutnamBench (660 problems), FATE-H and FATE-X (100 each), CombiBench, IMO 2025, Putnam 2025 and a subset of Erdős problems, under Lean v4.22.0.

The full workflow solves 87.9% of PutnamBench, 80% of Fate-H, 33% of Fate-X and 48% of CombiBench at 10 H20 days per problem, against AlphaProof's 56.1% at 500 TPU days and Seed-Prover 1.0's 50.4% at 18 H20 days. Over 1200 RL steps, batch accuracy went from ~50% to ~90% while average tool calls fell from ~15 to 10 and sequence length from ~28k to ~17k tokens. The agentic prover alone at pass@8×8 reached 359/660 Putnam and 57/100 Fate-H.

Compute budgets are reported but not matched across systems, and baselines are quoted from their own papers rather than rerun; there is no ablation separating the sketch model from the RL-trained prover. CombiBench and some Erdős formalizations are acknowledged as faulty, and the authors say the Erdős problems solved were simple or simplified.

Treat undergraduate and graduate formal proving as largely solved at moderate cost; PhD-level and research mathematics are not.

Written from the abstract by claude-opus-5 on 2026-10-17, with every figure checked against it. Not a substitute for the paper.

Referenced by

Claims in this catalog that draw on this source, and whether as support or counterpoint.

supportsA Lean prover trained with large-scale agentic reinforcement learning against the Lean checker, paired with a test-time workflow that drafts in natural language before formalizing, solved 88% of PutnamBench (undergraduate), 80% of Fate-H (graduate) and 33% of Fate-X (PhD-level), and 11 of 12 Putnam 2025 problems, at a smaller compute budget than prior systems, so formal proving at undergraduate level is largely solved while PhD-level remains open.