mlsanityData to 7 Oct 2026

STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving

arXiv 2502.00212 ↗First posted 31 Jan 2025cs.LG cs.AI cs.LOcited by 77

On the map: LLM reasoning → Mathematical reasoning

also in 1 more
Abstract (arXiv)

A fundamental challenge in formal theorem proving by LLMs is the lack of high-quality training data. Although reinforcement learning or expert iteration partially mitigates this issue by alternating between LLM generating proofs and finetuning them on correctly generated ones, performance quickly plateaus due to the scarcity of correct proofs (sparse rewards). To keep improving the models with limited data, we draw inspiration from mathematicians, who continuously develop new results, partly by proposing novel conjectures or exercises (which are often variants of known results) and attempting to solve them. We design the Self-play Theorem Prover (STP) that simultaneously takes on two roles, conjecturer and prover, each providing training signals to the other. The conjecturer is trained iteratively on previously generated conjectures that are barely provable by the current prover, which incentivizes it to generate increasingly challenging conjectures over time. The prover attempts to prove the conjectures with standard expert iteration. We evaluate STP with both Lean and Isabelle formal versifiers. With 51.3 billion tokens generated during the training in Lean, STP proves 28.5% of the statements in the LeanWorkbook dataset, doubling the previous best result of 13.2% achieved through expert iteration. The final model achieves state-of-the-art performance among whole-proof generation methods on miniF2F-test (65.0%, pass@3200), Proofnet-test (23.9%, pass@3200) and PutnamBench (8/644, pass@3200). We release our code, model, and dataset in this URL: https://github.com/kfdong/STP.

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

Builds on

46 of 64 references.

Closest ancestors · 7

Same direction, newest first

  1. 2024Formal Mathematical Reasoning: A New Frontier in AI20 Dec
  2. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically4 Nov
  3. 2024Lean-STaR: Learning to Interleave Thinking and Proving14 Jul
  4. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts3 Jul
  5. 2024Process-Driven Autoformalization in Lean 44 Jun
  6. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models5 Feb
  7. 2023Llemma: An Open Language Model For Mathematics16 Oct

Other references · 39

  1. 2023Llama 2: Open Foundation and Fine-Tuned Chat Modelscited by 12,865
  2. 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,355
  3. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,146
  4. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  5. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  6. 2017Hindsight Experience Replaycited by 1,096
  7. 2022CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesiscited by 876
  8. 2023StarCoder: may the source be with you!cited by 790
  9. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  10. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  11. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  12. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 245
27 more
  1. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  2. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  3. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  4. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  5. 2022Evolving Curricula with Regret-Based Environment Designcited by 166
  6. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  7. 2020Automatic Curriculum Learning For Deep RL: A Short Surveycited by 141
  8. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  9. 2024Multi-Step Reasoning with Large Language Models, a Surveycited by 140
  10. 2019The Lean mathematical librarycited by 127
  11. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  12. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  13. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  14. 2020Autotelic Agents with Intrinsically Motivated Goal-Conditioned Reinforcement Learning: a Short Surveycited by 83
  15. 2022Language Models Can Teach Themselves to Program Bettercited by 75
  16. 2018Reinforcement Learning of Theorem Provingcited by 69
  17. 2023OMNI: Open-endedness via Models of human Notions of Interestingnesscited by 66
  18. 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
  19. 2020INT: An Inequality Benchmark for Evaluating Generalization in Theorem Provingcited by 44
  20. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  21. 2023Multilingual Mathematical Autoformalizationcited by 38
  22. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  23. 2020First Neural Conjecturing Datasets and Experimentscited by 26
  24. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  25. 2018Dual Policy Iterationcited by 22
  26. 2024Scalable Reinforcement Post-Training Beyond Static Human Prompts: Evolving Alignment via Asymmetric Self-Playcited by 21
  27. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 39; 2026: 38.

77 papers.

Sort:

By area:

  1. 2025Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Modelscited by 381
  2. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  4. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  5. 2025ReMA: Learning to Meta-think for LLMs with Multi-Agent Reinforcement Learningcited by 78
  6. 2025Self-Challenging Language Model Agentscited by 56
  7. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  8. 2025Inference-time Scaling of Diffusion Models through Classical Searchcited by 48
  9. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  10. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  11. 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoningcited by 34
  12. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
38 more
  1. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  2. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  3. 2026Large Language Model Reasoning Failurescited by 20
  4. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  5. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 16
  6. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 13
  7. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  8. 2025StepFun-Prover Preview: Let's Think and Verify Step by Stepcited by 12
  9. 2025Let's Reason Formally: Natural-Formal Hybrid Reasoning Enhances LLM's Math Capabilitycited by 11
  10. 2025Learning to Generate Unit Test via Adversarial Reinforcement Learningcited by 11
  11. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  12. 2025A Survey of Scaling in Large Language Model Reasoningcited by 10
  13. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  14. 2025Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Provingcited by 10
  15. 2025AceSearcher: Bootstrapping Reasoning and Search for LLMs via Reinforced Self-Playcited by 10
  16. 2026Scaling Self-Play with Self-Guidancecited by 9
  17. 2025Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalitiescited by 8
  18. 2025Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selectioncited by 8
  19. 2025SPARQ: Synthetic Problem Generation for Reasoning via Quality-Diversity Algorithmscited by 7
  20. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficultycited by 7
  21. 2026LongCat-Flash-Prover: Advancing Native Formal Reasoning via Agentic Tool-Integrated Reinforcement Learningcited by 6
  22. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 6
  23. 2026Autonomous Research Agents: A Survey of AI Scientists and the Verification Gapcited by 6
  24. 2025GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Provingcited by 5
  25. 2025Teaching Language Models to Reason with Toolscited by 5
  26. 2025Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4cited by 5
  27. 2026TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?cited by 5
  28. 2026Process-Verified Reinforcement Learning for Theorem Proving via Leancited by 5
  29. 2026GASP: Guided Asymmetric Self-Play For Coding LLMscited by 4
  30. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 4
  31. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4
  32. 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Examcited by 3
  33. 2026A Deep Dive into Scaling RL for Code Generation with Synthetic Data and Curriculacited by 3
  34. 2026Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systemscited by 3
  35. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 3
  36. 2025Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Provingcited by 2
  37. 2025Discovering New Theorems via LLMs with In-Context Proof Learning in Leancited by 2
  38. 2025Learning Interestingness in Automated Mathematical Theory Formationcited by 2

50 most cited of 77 All 77 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
  2. 2021Learning Equational Theorem Proving
  3. 2025Theorem Prover as a Judge for Synthetic Data Generation
  4. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  5. 2025DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
  6. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning
  7. 2025Towards Understanding Self-play for LLM Reasoning
  8. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance