PaperlayerView exact revision on arXiv

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

arXiv:2507.23726v2cs.AIcs.CL

TL;DR

Automatically verifying natural-language proofs is difficult because each step must be checked, complicating reinforcement-learning supervision for theorem proving. Seed-Prover centers formal reasoning on lemmas and refines proofs using Lean feedback, while the paper reports that its formal systems substantially outperform previous frameworks and prove 5 of 6 IMO 2025 problems.

  • Problem

    Automatically verifying natural-language proofs is difficult because each proof step must be checked, while Lean offers an automatic correctness signal for formalized proofs.

    Source: §1 · p. 2

  • Method

    Seed-Prover centers formal reasoning on independently provable, combinable lemmas and iteratively refines proofs using Lean feedback, proved lemmas, and self-summarization, with three-tiered test-time inference.

    Source: §1 · p. 2, §2.2 · p. 4

  • Results

    Both systems substantially outperform previous formal reasoning frameworks, and Seed-Prover proves 5 of 6 problems in IMO 2025.

    Source: §4 · p. 9

  • Takeaways & Limitations

    The IMO 2025 proofs demonstrate the efficacy of formal reasoning systems integrating large language models.

    Source: §4 · p. 9

Abstract

from arXiv · show

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

The introduction argues that Lean provides automatic correctness signals where natural-language proof verification is difficult, and presents Seed-Prover’s whole-proof approach alongside a dedicated geometry engine.

Motivation

  • Step-level Lean provers [14] [22] [23] interact incrementally but need scaffolding; whole-proof models [5, 24] lack compiler interaction, while long chain-of-thought combinations outperform them [9] [15] [21].The introduction notes that natural-language proofs are difficult to verify step by step, whereas Lean automatically signals formal proof correctness.Source: §1 · p. 2

Seed-Prover

  • Seed-Prover generates intermediate lemmas shared across inference paths and iteratively refines proofs using Lean feedback, previously proved lemmas, and self-summarization.Source: §1 · p. 2
  • Its three-tiered test-time inference strategy allocates reasoning to fine details while exploring promising properties, enabling both deep and broad search.Source: §1 · p. 2

Seed-Prover results

  • Seed-Prover proves 5 out of 6 IMO 2025 problems, saturates MiniF2F, and outperforms prior work by up to 3× on multiple formal benchmarks.The MiniF2F result is shown in Figure 1.Source: §1 · p. 2

Seed-Geometry results

  • Seed-Geometry solves 43 IMO-AG-50 problems versus 42 by AlphaGeometry 2 [2], sets a new shortlist geometry state of the art, and solves IMO 2025 geometry in under 2 seconds.IMO-AG-50 curates IMO geometry problems from 2000 to 2024; the shortlist result covers 2000 to 2022.Source: §1 · p. 2

Seed-Geometry

  • Seed-Geometry forward-chains applicable rules to closure, backward-traces fact dependencies, and uses a 230-million-problem repository to train a model that supplies auxiliary geometry elements.The engine separates problem context from auxiliary constructions, then completes proofs through step-by-step forward-chaining.Source: §1 · p. 2

2 Approach

The approach introduces Seed-Geometry and Seed-Prover, the two systems used in IMO 2025.

  • Seed-Geometry is one of the two systems introduced for use in IMO 2025.Source: §2 · p. 2
  • Seed-Prover is the other system introduced for use in IMO 2025.Source: §2 · p. 2

2.1 Seed-Geometry

Seed-Geometry substantially redesigns TongGeometry while retaining neural auxiliary-construction proposals and specialized forward-chaining reasoning engines. Its approach combines concise construction actions, a faster backend, a single Seed-family policy model, and an extensive search process.

2.1 Seed-Geometry

  • Seed-Geometry substantially redesigns TongGeometry [30], retaining neural models for missing auxiliary constructions and specialized engines for forward-chaining derivation.The paper describes Seed-Geometry as a substantial upgrade over TongGeometry.Source: §2.1 · pp. 2–3

2.1.1 Extended Domain-Specific Language

  • Seed-Geometry groups cumbersome ruler-and-compass sequences into concise composite actions, including isogonal conjugates and the exsimilitude and insimilitude centers of two circles.These constructions can be expressed with primitive ruler-and-compass actions, but their sequences are non-trivial and clumsy.Source: §2.1.1 · p. 3

2.1.2 Extremely Fast Reasoning Engine

  • A C++ backend exposed to Python through Pybind11 delivers roughly 100-fold speedup over TongGeometry’s Python implementation, enabling faster deep searches as trees widen.The C++ implementation handles memory more efficiently and benefits from compiler optimizations.Source: §2.1.2 · p. 3

2.1.3 Exceptional Large Language Model

  • A pretrained Seed-family model [17] serves as the sole policy for proposing auxiliary constructions, without target-goal facts in its prompt, after preliminary experiments found a value model unnecessary.The model was extensively pretrained on coding and mathematics, and its size was chosen in light of the number of data tokens.Source: §2.1.3 · p. 3

2.1.4 Extensive Search

  • Seed-Geometry canonicalizes problems, first tries backend reasoning, then uses beam search to propose auxiliary constructions and expand top candidates by cumulative negative log likelihood until a fixed step limit.GPU processes can run in a distributed setup, while CPU thread pools asynchronously execute reasoning to overlap its cost with language-model inference.Source: §2.1.4 · p. 3

2.2 Seed-Prover

Seed-Prover centers both training and inference on lemma-style proof generation, then combines conjecture exploration and iterative refinement to tackle difficult Lean problems. Its test-time strategies range from refining proofs to exploring large pools of candidate lemmas.

2.2.1 Lemma-Style Proving

  • Seed-Prover’s defining approach generates and proves lemmas before applying them in the main theorem, making proof progress explicit and enabling modular combination of lemmas.A per-problem lemma pool stores statements, names, proofs, proof difficulties, and dependency relations for retrieval and further work.Source: §2.2 · p. 4, §2.2.1 · p. 4

2.2.2 Conjecture Proposing

  • The proposer explores broadly by generating 10–50 candidate conjectures, optionally using proved lemmas, and can be repeated to build a large pool of potential properties.This exploration can uncover useful properties that enable solutions to problems the model cannot solve directly in natural language.Source: §2.2.2 · pp. 4–5

2.2.3 Training

  • Training uses multi-stage, multi-task reinforcement learning with a binary proof reward, progressively harder problems, and diverse prompts that include Lean feedback and prior attempts.The dataset includes open-source and in-house formalized problems, easier variants of difficult problems, and excludes problems with proof rates above 1/4.Source: §2.2.3 · p. 5

2.2.4 Test-Time Scaling

  • Under light inference, up to 8–16 Lean-feedback refinements with self-summarization yield a Pass@64–256-equivalent budget; Seed-Prover proves IMO 2022 P2 (MOHS = 151), versus Pass@8192 without refinement.Refinement often fixes Lean syntax errors or changes the initial proof sketch’s reasoning trajectory.Source: §2.2.4 · pp. 5–6
  • Medium inference combines outer refinement of the main proof with inner 8 × 8 light refinement of difficult lemmas, solving IMO 2003 P6, IMO 2020 P5, IMO 2024 P1, and IMO 2025 P5.Final proofs can exceed 1000 lines of code.Source: §2.2.4 · p. 6
  • Heavy inference starts with 5000 conjectures, proves or disproves them under light inference, and ranks resulting lemmas for a medium-setting proof; it solves IMO 2017 P2, IMO 2025 P3, and IMO 2025 P4.After days of inference, the lemma pool can contain several thousand facts; ranking uses proof rate, semantic relevance, and proof length, with low proof rate often indicating crucial lemmas.Source: §2.2.4 · p. 6

3 Evaluation

Evaluation reports Seed-Prover’s results across past IMO problems and formal-math benchmarks, alongside Seed-Geometry’s performance on IMO geometry problems. Seed-Prover proves 121/155 past IMO problems, while Seed-Geometry solves 43 IMO geometry problems from 2000–2024 and 22 IMO shortlist problems.

3.1 Seed-Geometry

  • Seed-Geometry solves 43 IMO geometry problems from 2000–2024, one more than AlphaGeometry 2.Its generation program found over 230 million unique problems in more than seven days at 8x the search efficiency of the Python implementation; the final evaluation used distributed step-by-step generation with beam search.Source: Table 1 · p. 7, §3.1 · p. 7
  • On the IMO shortlist from 2000–2022, Seed-Geometry solves 22/39 problems, compared with AlphaGeometry 2’s 19/39.The comparison includes all hard-level shortlist problems, and Seed-Geometry solved IMO 2025 P2 in 2 seconds after receiving a human-provided formulation.Source: §3.1 · p. 7, Table 2 · p. 8

3.2 Seed-Prover

  • Seed-Prover proves 121/155 past IMO problems (78.1%), including 47/55 easy, 47/56 medium, and 27/44 hard problems.By subject, it proves 72/85 algebra, 42/55 number theory, and 7/14 combinatorics problems.Source: Table 3 · p. 8, §3.2 · p. 9
  • At medium inference, Seed-Prover proves 99.6% of problems in both MiniF2F-valid and MiniF2F-test.With heavy inference, it proves IMO 1990 P3 but fails on IMOSL 2007 Algebra P6.Source: Table 3 · p. 8, §3.2 · p. 9
  • On PutnamBench, Seed-Prover proves 201/657 problems with light inference and 331/657 with medium inference.The paper describes the medium-setting result as a significant performance jump over previous work.Source: Table 3 · p. 8, §3.2 · p. 9
  • At medium inference, Seed-Prover proves 30/100 CombiBench problems, outperforming previous work while still struggling with combinatorics relative to other benchmarks.Source: Table 3 · p. 8, §3.2 · p. 9
  • On MiniCTX-v2, Seed-Prover achieves 81.8%, compared with o4-mini’s 44.3% of statements at Pass@8.MiniCTX-v2 contains context-rich problems written after November 2024; evaluation used light inference under Lean v4.16.0.Source: Table 3 · p. 8, §3.2 · p. 9
  • At IMO 2025, Seed-Geometry solved Problem 2 instantly; Seed-Prover solved Problem 5 with medium inference and required heavy inference for Problems 1, 3, and 4.The Problem 1 proof was completed after the submission deadline.Source: §3.2 · p. 8

4 Conclusion

Seed-Geometry and Seed-Prover substantially outperform previous formal reasoning frameworks, and together proved 5 of 6 problems in IMO 2025. The conclusion highlights their methods and Lean verification, while identifying open conjectures as a future target.

  • 5 of 6 problems in IMO 2025 were proved using Seed-Geometry and Seed-Prover, demonstrating the efficacy of these formal systems.Source: §4 · p. 9
  • Seed-Geometry accelerates verification and scales search, while Seed-Prover uses iterative refinement and three-tiered test-time inference to achieve state-of-the-art.The paper states that both systems substantially outperform previous formal reasoning frameworks.Source: §4 · p. 9
  • Lean enables rapid proof verification, making formal languages more cost-effective than human experts and more reliable than LLM judges.Source: §4 · p. 9
  • Future work will combine formal systems with large language models to tackle open conjectures.Source: §4 · p. 9

Appendix · B LooKeng: An Easy-to-Use and Effective Python Interface for Lean

LooKeng is a REPL4-based Python interface that addresses LeanDojo’s version and repository requirements while simplifying Lean interaction for development and inference. Its features support proof execution, verification, scaling, and resource management.

B LooKeng: An Easy-to-Use and Effective Python Interface for Lean

Related papers

Loading 2507.23726v2…