Source-linked AI summary
Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, Cheng Ren, Jiawei Shen, Wenlei Shi, Tong Sun, He Sun, Jiahui Wang, Siran Wang, Zhihong Wang, Chenrui Wei, Shufa Wei, Yonghui Wu, Yuchen Wu, Yihang Xia, Huajian Xin, Fan Yang, Huaiyuan Ying, Hongyi Yuan, Zheng Yuan, Tianyang Zhan, Chi Zhang, Yue Zhang, Ge Zhang, Tianyun Zhao, Jianqiu Zhao, Yichi Zhou, Thomas Hanwen Zhu
TL;DR
The paper addresses the weak supervision available for theorem proving from natural language by using Lean’s formal verification. It introduces lemma-centered Seed-Prover with iterative refinement and deep-and-broad test-time inference, alongside Seed-Geometry for geometry. These systems prove 78.1% of formalized past IMO problems and 5 of 6 IMO 2025 problems while outperforming prior formal reasoning systems.
Problem
Natural-language proofs provide no clear automatic correctness signal for reinforcement learning, whereas formal theorem proving requires checking each proof step.
Method
Seed-Prover uses lemma-style whole-proof reasoning, iterative refinement from Lean feedback and summaries, and three-tier inference; Seed-Geometry supplies a dedicated geometry engine.
Results
Seed-Prover proves 78.1% of formalized past IMO problems, and the combined systems prove 5 of 6 IMO 2025 problems while outperforming previous formal reasoning frameworks.
Takeaways & Limitations
The results demonstrate that formal verification can support long chain-of-thought reasoning for automated mathematical problem solving.
Abstract
from arXiv · showhide
LLMs have demonstrated strong mathematical reasoning abilities by leveraging reinforcement learning with long chain-of-thought, yet they continue to struggle with theorem proving due to the lack of clear supervision signals when solely using natural language. Dedicated domain-specific languages like Lean provide clear supervision via formal verification of proofs, enabling effective training through reinforcement learning. In this work, we propose \textbf{Seed-Prover}, a lemma-style whole-proof reasoning model. Seed-Prover can iteratively refine its proof based on Lean feedback, proved lemmas, and self-summarization. To solve IMO-level contest problems, we design three test-time inference strategies that enable both deep and broad reasoning. Seed-Prover proves $78.1\%$ of formalized past IMO problems, saturates MiniF2F, and achieves over 50\% on PutnamBench, outperforming the previous state-of-the-art by a large margin. To address the lack of geometry support in Lean, we introduce a geometry reasoning engine \textbf{Seed-Geometry}, which outperforms previous formal geometry engines. We use these two systems to participate in IMO 2025 and fully prove 5 out of 6 problems. This work represents a significant advancement in automated mathematical reasoning, demonstrating the effectiveness of formal verification with long chain-of-thought reasoning.
1 Introduction
Seed-Prover addresses the difficulty of training theorem provers from natural-language proofs by using Lean’s formal verification signals. Its lemma-centered refinement and tiered inference strategies achieve strong results on formal mathematics and geometry.
- Lean provides an automatic correctness signal for formal proofs, unlike natural-language proofs whose individual steps are difficult to verify.
- Seed-Prover generates intermediate lemmas, then iteratively refines proofs using Lean feedback, proved lemmas, and self-summarization.
- Three-tier test-time inference allocates computation for both detailed reasoning and broad exploration of potentially useful properties.
- 5 out of 6 IMO 2025 problems were proved, while MiniF2F was saturated and prior work was outperformed by up to 3× on multiple formal benchmarks.
- Seed-Geometry adds a dedicated geometry reasoning engine because Lean lacks sufficient geometry support.
- Seed-Geometry establishes a new state-of-the-art on IMO shortlist geometry problems and solves the IMO 2025 geometry problem in under 2 seconds.
2 Approach
The paper introduces Seed-Geometry and Seed-Prover as two formal reasoning systems that integrate large language models for mathematical problem solving.
- Seed-Geometry and Seed-Prover are the two formal reasoning systems used in the paper’s IMO 2025 participation.
2.1 Seed-Geometry
Seed-Geometry combines neural proposal generation with a specialized forward-chaining engine and scalable search. Its redesigned implementation reduces representation and computation costs for difficult geometry problems.
- Seed-Geometry substantially upgrades TongGeometry while retaining trained neural models and specialized forward-chaining reasoning engines.
- Grouped construction actions make ruler-and-compass diagrams more concise for neural processing and symbolic derivation.
- A C++ backend delivers roughly a 100-fold speed increase over TongGeometry’s Python implementation, enabling deeper searches.
- The system uses a Seed-family language model to propose auxiliary geometric elements for construction.
- Seed-Geometry canonicalizes each problem, checks whether the goal fact is reachable, and otherwise launches beam search over model proposals.
2.2 Seed-Prover
Seed-Prover centers formal reasoning on independently compilable lemmas, then combines iterative refinement with broad conjecture exploration and tiered test-time search. These mechanisms support proofs of increasingly difficult contest problems.
- 2.2 Seed-Prover: Lemma-style proving makes lemmas central to training and inference, allowing progress tracking, independent processing, and combination across inference trajectories.
- 2.2.2 Conjecture Proposing: Seed-Prover proposes properties such as injectivity or monotonicity to explore a problem broadly before committing to a complete proof.
- 2.2.2 Conjecture Proposing: Unlike approaches that assume a complete solution upfront, broad exploratory search can discover useful properties for problems the model cannot solve directly in natural language.
- 2.2 Seed-Prover: Reinforcement learning rewards successful formal proofs and uses formatting penalties, progressively increasing difficulty, data quality, and output length.
- 2.2.4 Test-Time Scaling: Light inference refines each proof up to 8–16 times with Lean feedback and self-summarization, equivalent to whole-proof sampling at Pass@64–256.
- 2.2.4 Test-Time Scaling: Medium inference adds inner refinement for difficult generated lemmas and solves IMO 2003 P6, IMO 2020 P5, IMO 2024 P1, and IMO 2025 P5.
- 2.2.4 Test-Time Scaling: Heavy inference begins with thousands of conjectures, proving or disproving them with the light setting and moving successful conjectures into a lemma pool.
3 Evaluation
The evaluation spans geometry, contest, benchmark, and real-world formalization tasks. Seed-Geometry and Seed-Prover achieve strong results across these settings, while combinatorics remains comparatively challenging.
- Seed-Geometry: 43 solutions on IMO geometry problems from 2000 to 2024 put Seed-Geometry one solution ahead of AlphaGeometry 2.On the harder 2000–2022 IMO shortlist, Seed-Geometry solved 22 of 39 problems versus AlphaGeometry 2’s 19.
- Seed-Geometry: 22 of 39 IMO shortlist geometry problems were solved by Seed-Geometry, compared with 19 solved by AlphaGeometry 2.The comparison includes hard problems omitted from the original IMOSL-AG-30 benchmark.
- Evaluation setup: The evaluation used multiple inference settings across IMO 2025, past IMO problems, MiniF2F, PutnamBench, CombiBench, and MiniCTX-v2.Unless otherwise specified, experiments used Lean v4.14.0 with its corresponding Mathlib version.
- Seed-Prover: 78.1% of formalized past IMO problems were proved by Seed-Prover, including 121 of 155 problems.The system proved 47/55 easy, 47/56 medium, and 27/44 hard problems across algebra, number theory, and combinatorics.
- Seed-Prover: 99.6% of problems were proved on both MiniF2F-valid and MiniF2F-test under the medium setting.Heavy inference solved the final problem in one split but failed on the final problem in the other.
- Seed-Prover: 331/657 PutnamBench problems were proved with medium inference, up from 201/657 with light inference.The paper describes this as a significant performance jump compared with previous work on undergraduate mathematics problems.
- Seed-Prover: 30 out of 100 CombiBench problems were proved, outperforming previous work but still indicating difficulty with combinatorics.CombiBench focuses on combinatorial problems involving newly defined concepts.
- Seed-Prover: 81.8% of MiniCTX-v2 statements were solved under light inference, compared with 44.3% for o4-mini at Pass@8.MiniCTX-v2 contains post-November-2024 context-rich problems from real-world formalization repositories.
4 Conclusion
The paper presents Seed-Geometry and Seed-Prover as formal reasoning frameworks integrating large language models. They combine geometry search and iterative proof refinement to achieve strong formal reasoning results, including five of six IMO 2025 problems.
- Frameworks: Seed-Geometry and Seed-Prover integrate large language models into formal reasoning frameworks.The systems are presented as substantially outperforming previous formal reasoning frameworks.
- Approach: Seed-Geometry accelerates verification and scales the search mechanism, while Seed-Prover uses iterative refinement and three-tiered test-time inference.These design choices are summarized as supporting Seed-Prover’s state-of-the-art performance.
- Results: 5 out of 6 IMO 2025 problems were formally proved.The conclusion identifies this result as evidence of the efficacy of the formal systems.
- Implications: Lean provides rapid proof verification that the paper describes as more cost-effective than human experts and more reliable than LLM judges.The stated future direction is combining formal systems with language models to tackle open conjectures.
A Contributors
The contributor list assigns work across algorithm, data, and infrastructure roles.
- Algorithm: The Algorithm contributors are Luoxin Chen, Liankai Huang, Zhicheng Jiang, and the listed collaborators.The paper separately identifies Data and Infra contributor groups.
- Data: The Data contributors are Jinming Gu, Wenhao Huang, Zhicheng Jiang, and the listed collaborators.The list includes contributors marked with an asterisk as having left Seed.
- Infra: The Infra contributors are Cheng Ren, He Sun, Zhihong Wang, Tianyun Zhao, Jianqiu Zhao, and Thomas Hanwen Zhu.The asterisk marks a member who left Seed.
B LooKeng: An Easy-to-Use and Effective Python Interface for Lean
LooKeng is a Python-facing Lean interface designed for scalable interaction and reliable proof verification. It supports both step-by-step interaction and direct whole-proof verification across Lean versions.
- Motivation: LooKeng addresses Lean interaction constraints involving older LeanDojo support and repository creation at development scale.The interface is intended to make large-scale Lean interaction more practical.
- Interface: LooKeng supports both step-by-step Lean interaction and direct verification of an entire proof.Its key features are presented as an easy-to-use interface for Lean workflows.
- Scalability: A stateless design lets different LooKeng instances process the same Lean state simultaneously for scaling and sharing.The service can also handle thousands of concurrent requests through asynchronous architecture and resource isolation.
- Operational features: LooKeng supports complex tactics, multiple Lean versions, memory thresholds, and automatic process termination when limits are exceeded.These features target robust operation across heterogeneous Lean workflows.
- Proof utilities: The verify_proof method rigorously checks final proofs through Lean’s native interface, while proof simplification removes useless tactics and hypotheses.LooKeng can also generate a statement’s negation.