The Year in AI Papers
The year/Independent research

Paper 2512.17260

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, et al.

Published
Dec 2025
Research lab
Independent
Citations
29
GitHub
Not linked

01 In brief

Summary

Seed-Prover 1.5 is a formal theorem-proving system for Lean developed by ByteDance Seed AI4Math.

It uses an agentic prover trained via large-scale reinforcement learning (RL) with tool integration (Lean verification, Mathlib search, Python execution) and a sketch model trained with rubric RL to bridge natural language proofs and Lean sketches.

The system achieves state-of-the-art results: 88% on PutnamBench, 80% on Fate-H, and 33% on Fate-X, and solved 11 of 12 Putnam 2025 problems within 9 hours.

Compared to prior methods like AlphaProof and Hilbert, it uses a smaller compute budget.

Key innovations include incremental lemma caching, adaptive tool use, and a hierarchical test-time workflow with three agents (natural language prover, sketch model, agentic Lean prover).

RL training improved accuracy from ~50% to ~90% and reduced average sequence length from ~28k to ~17k tokens.

The system still struggles with PhD-level problems and frontier research, facing a 'dependency issue' requiring synthesis of multiple papers.

02 From the paper

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.