mlsanityData to 7 Oct 2026

Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

arXiv 2508.03613 ↗First posted 5 Aug 2025cs.LG cs.AIcited by 140

On the map: Synthetic data and self-improvement for LLMs → Self-play RL for reasoning

Abstract (arXiv)

We introduce Goedel-Prover-V2, a series of open-source language models that set a new state-of-the-art in automated theorem proving. Built on the standard expert iteration and reinforcement learning pipeline, our approach incorporates three key innovations: (1) Scaffolded data synthesis: We generate synthetic tasks of increasing difficulty to train the model to master increasingly complex theorems; (2) Verifier-guided self-correction: We enable the model to iteratively revise its proofs by leveraging feedback from the Lean compiler; (3) Model averaging: We merge model checkpoints to mitigate the decrease in model output diversity in later stages of training. Our small model, Goedel-Prover-V2-8B, reaches 84.6% pass@32 on MiniF2F and outperforms DeepSeek-Prover-V2-671B under the same metric, despite being 80X smaller. Our flagship model, Goedel-Prover-V2-32B, achieves 88.1% on MiniF2F at pass@32 in standard mode and 90.4% in self-correction mode, outperforming prior SOTA by a large margin. Additionally, our flagship model solves 86 problems on PutnamBench at pass@184, securing the first place among open-source models on the leaderboard, surpassing DeepSeek-Prover-V2-671B's record of solving 47 problems by pass@1024 with a significantly smaller model size and compute budget. At the time of its release (July-August 2025), Goedel-Prover-V2 achieves the strongest overall performance among all open-source theorem provers. It also ranks among the top-performing models--including closed-source systems with publicly reported performance--under a constrained test-time compute budget. Our models, code, and data are released at https://github.com/Goedel-LM/Goedel-Prover-V2.

Key facts. Cited by 140 papers in the map (data through 7 Oct 2026). Placed in Self-play RL for reasoning, one of 13 directions in Synthetic data and self-improvement for LLMs. Builds on 43 of its 86 references that are in the map. First posted on arXiv 5 Aug 2025.

Builds on

43 of 86 references.

Closest ancestors · 3

Same direction, newest first

  1. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan
  2. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving30 Dec
  3. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data23 May

Other references · 40

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  2. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  3. 2025Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilitiescited by 3,655
  4. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,155
  5. 2025DAPO: An Open-Source LLM Reinforcement Learning System at Scalecited by 2,678
  6. 2024HybridFlow: A Flexible and Efficient RLHF Frameworkcited by 1,980
  7. 2024Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameterscited by 1,928
  8. 2024LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Modelscited by 1,442
  9. 2022Model soups: averaging weights of multiple fine-tuned models improves accuracy without increasing inference timecited by 1,366
  10. 2025Understanding R1-Zero-Like Training: A Critical Perspectivecited by 1,276
  11. 2023Teaching Large Language Models to Self-Debugcited by 963
  12. 2025Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?cited by 948
28 more
  1. 2021Robust fine-tuning of zero-shot modelscited by 785
  2. 2023YaRN: Efficient Context Window Extension of Large Language Modelscited by 584
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  5. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  6. 2024Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Modelscited by 277
  7. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  8. 2024RepairAgent: An Autonomous, LLM-Based Agent for Program Repaircited by 225
  9. 2023Is Self-Repair a Silver Bullet for Code Generation?cited by 191
  10. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  11. 2023Mitigating the Alignment Tax of RLHFcited by 181
  12. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  13. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  14. 2025AIMO-2 Winning Solution: Building State-of-the-Art Mathematical Reasoning Models with OpenMathReasoning datasetcited by 165
  15. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  16. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  17. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  18. 2025Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2cited by 95
  19. 2024Metacognitive Capabilities of LLMs: An Exploration in Mathematical Problem Solvingcited by 82
  20. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  21. 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 72
  22. 2023FIMO: A Challenge Formal Dataset for Automated Theorem Provingcited by 54
  23. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  24. 2024A Semantic Search Engine for Mathlib4cited by 30
  25. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  26. 2023Spurious Feature Diversification Improves Out-of-distribution Generalizationcited by 26
  27. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  28. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17

Built on by

Cited by year (2026 to 7 Oct)

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

140 papers.

Sort:

By area:

  1. 2025WoW: Towards a World omniscient World model Through Embodied Interactioncited by 66
  2. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  3. 2025AdvancedIF: Rubric-Based Benchmarking and Reinforcement Learning for Advancing LLM Instruction Followingcited by 46
  4. 2026Code as Agent Harnesscited by 40
  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. 2025Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skillscited by 19
  10. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  11. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  12. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
38 more
  1. 2025DRPO: Efficient Reasoning via Decoupled Reward Policy Optimizationcited by 16
  2. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 15
  3. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  4. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 13
  5. 2026R3L: Reflect-then-Retry Reinforcement Learning with Language-Guided Exploration, Pivotal Credit, and Positive Amplificationcited by 12
  6. 2025IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generationcited by 11
  7. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  8. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  9. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 10
  10. 2026Scaling Self-Play with Self-Guidancecited by 9
  11. 2025ASSESS: A Semantic and Structural Evaluation Framework for Statement Similaritycited by 8
  12. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  13. 2025HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMscited by 8
  14. 2026MerLean: An Agentic Framework for Autoformalization in Quantum Computationcited by 8
  15. 2026Escaping the Cognitive Well: Efficient Competition Math with Off-the-Shelf Modelscited by 8
  16. 2025LeanGeo: Formalizing Competitional Geometry problems in Leancited by 7
  17. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficultycited by 7
  18. 2025Autoformalizer with Tool Feedbackcited by 7
  19. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  20. 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinementcited by 7
  21. 2026Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Provingcited by 7
  22. 2026VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Leancited by 6
  23. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 6
  24. 2026Delay, Plateau, or Collapse: Evaluating the Impact of Systematic Verification Error on RLVRcited by 6
  25. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 6
  26. 2025Automated Formalization via Conceptual Retrieval-Augmented LLMscited by 5
  27. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  28. 2025GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Provingcited by 5
  29. 2025Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4cited by 5
  30. 2026Automatic Textbook Formalizationcited by 5
  31. 2026Formal Conjectures: An Open and Evolving Benchmark for Verified Discovery in Mathematicscited by 5
  32. 2026Process-Verified Reinforcement Learning for Theorem Proving via Leancited by 5
  33. 2025DAG-Math: Graph-of-Thought Guided Mathematical Reasoning in LLMscited by 4
  34. 2025LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)cited by 4
  35. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?cited by 4
  36. 2026The Agentic Researcher: A Practical Guide to AI-Assisted Research in Mathematics and Machine Learningcited by 4
  37. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 4
  38. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4

50 most cited of 140 All 140 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025Theorem Prover as a Judge for Synthetic Data Generation
  2. 2026Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
  3. 2025EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving
  4. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoning
  5. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
  6. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  7. 2025FormaRL: Enhancing Autoformalization with no Labeled Data
  8. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation