mlsanityData to 7 Oct 2026

Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving

arXiv 2507.23726 ↗First posted 31 Jul 2025cs.AI cs.CLcited by 96

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

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 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 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.

Key facts. Cited by 96 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 24 of its 28 references that are in the map. First posted on arXiv 31 Jul 2025.

Builds on

24 of 28 references.

Closest ancestors · 6

Same direction, newest first

  1. 2025Solving Formal Math Problems by Decomposition and Iterative Reflection21 Jul
  2. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics6 May
  3. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition30 Apr
  4. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning15 Apr
  5. 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad27 Mar
  6. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan

Other references · 18

  1. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,146
  2. 2015Neural Machine Translation of Rare Words with Subword Unitscited by 2,898
  3. 2025DAPO: An Open-Source LLM Reinforcement Learning System at Scalecited by 2,678
  4. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  6. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  7. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  8. 2025Seed1.5-Thinking: Advancing Superb Reasoning Models with Reinforcement Learningcited by 159
  9. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  10. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  11. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  12. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
6 more
  1. 2025Big-Math: A Large-Scale, High-Quality Math Dataset for Reinforcement Learning in Language Modelscited by 104
  2. 2025Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2cited by 95
  3. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  4. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  5. 2024Proposing and solving olympiad geometry with guided tree searchcited by 18
  6. 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalizationcited by 15

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 36; 2026: 60.

96 papers.

Sort:

By area:

  1. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 195
  2. 2025DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoningcited by 84
  3. 2025Breaking the Exploration Bottleneck: Rubric-Scaffolded Reinforcement Learning for General LLM Reasoningcited by 56
  4. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  5. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  6. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  7. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  8. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
  9. 2025Introducing LongCat-Flash-Thinking: A Technical Reportcited by 21
  10. 2025The FM Agentcited by 20
  11. 2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 19
  12. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
38 more
  1. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  2. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
  3. 2025DiFFPO: Training Diffusion LLMs to Reason Fast and Furious via Reinforcement Learningcited by 17
  4. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  5. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  6. 2026R-Diverse: Mitigating Diversity Illusion in Self-Play LLM Trainingcited by 9
  7. 2026Scaling Self-Play with Self-Guidancecited by 9
  8. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  9. 2025HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMscited by 8
  10. 2026Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibriumcited by 7
  11. 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinementcited by 7
  12. 2025Achieving Olympiad-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learningcited by 6
  13. 2026Learning to Repair Lean Proofs from Compiler Feedbackcited by 6
  14. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 6
  15. 2026Autonomous Research Agents: A Survey of AI Scientists and the Verification Gapcited by 6
  16. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  17. 2025LANPO: Bootstrapping Language and Numerical Feedback for Reinforcement Learning in LLMscited by 5
  18. 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 5
  19. 2026Formalizing Mathematics at Scalecited by 5
  20. 2025Intern-S1-MO: Long-horizon Reasoning Agent for Olympiad?Level Mathematical Problem Solvingcited by 4
  21. 2026Training LLMs for Divide-and-Conquer Reasoning Elevates Test-Time Scalabilitycited by 4
  22. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?cited by 4
  23. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 4
  24. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4
  25. 2026AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilitiescited by 4
  26. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematicscited by 4
  27. 2025Deep Self-Evolving Reasoningcited by 3
  28. 2025Honesty over Accuracy: Trustworthy Language Models through Reinforced Hesitationcited by 3
  29. 2025IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touchcited by 3
  30. 2026MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematicscited by 3
  31. 2026Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediariescited by 3
  32. 2026Agentic Proving for Program Verificationcited by 3
  33. 2026Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Leancited by 3
  34. 2025Discovering New Theorems via LLMs with In-Context Proof Learning in Leancited by 2
  35. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  36. 2025Pessimistic Verification for Open Ended Math Questionscited by 2
  37. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  38. 2025MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classificationcited by 2

50 most cited of 96 All 96 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
  2. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoning
  3. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
  4. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  5. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
  6. 2025StepFun-Prover Preview: Let's Think and Verify Step by Step
  7. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs
  8. 2025LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving