mlsanityData to 14 Oct 2026

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

arXiv 2504.06122 ↗First posted 8 Apr 2025cs.AIcited by 27

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages. To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.

Key facts. Cited by 27 papers in the map (data through 14 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 26 of its 51 references that are in the map. First posted on arXiv 8 Apr 2025.

Builds on

26 of 51 references.

Closest ancestors · 10

Same direction, newest first

  1. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving5 Mar
  2. 2025PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models4 Mar
  3. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan
  4. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving30 Dec
  5. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover24 Jul
  6. 2024Lean-STaR: Learning to Interleave Thinking and Proving14 Jul
  7. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts3 Jul
  8. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models5 Feb
  9. 2023Llemma: An Open Language Model For Mathematics16 Oct
  10. 2020Generative Language Modeling for Automated Theorem Proving7 Sep

Other references · 16

  1. 2023Direct Preference Optimization: Your Language Model is Secretly a Reward Modelcited by 8,065
  2. 2025DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learningcited by 6,330
  3. 2025Understanding R1-Zero-Like Training: A Critical Perspectivecited by 1,345
  4. 2024Qwen2.5-Coder Technical Reportcited by 1,203
  5. 2025SimpleRL-Zoo: Investigating and Taming Zero Reinforcement Learning for Open Base Models in the Wildcited by 511
  6. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  7. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  8. 2025Cognitive Behaviors that Enable Self-Improving Reasoners, or, Four Habits of Highly Effective STaRscited by 377
  9. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
  10. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  11. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 197
  12. 2022Formal Mathematics Statement Curriculum Learningcited by 142
4 more
  1. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  2. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 122
  3. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 84
  4. 2025ReMA: Learning to Meta-think for LLMs with Multi-Agent Reinforcement Learningcited by 79

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 21; 2026: 6.

27 papers.

Sort:

By area:

  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  2. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 205
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  4. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 80
  5. 2025Aristotle: IMO-level Automated Theorem Provingcited by 58
  6. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  7. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 31
  8. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 31
  9. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 27
  10. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  11. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 18
  12. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
15 more
  1. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 16
  2. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  3. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficultycited by 7
  4. 2025Achieving Olympiad-Level Geometry Large Language Model Agent via Complexity Boosting Reinforcement Learningcited by 7
  5. 2026Process-Verified Reinforcement Learning for Theorem Proving via Leancited by 7
  6. 2025LogicPuzzleRL: Cultivating Robust Mathematical Reasoning in LLMs via Reinforcement Learningcited by 5
  7. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  8. 2025Putting on the Thinking Hats: A Survey on Chain of Thought Fine-tuning from the Perspective of Human Reasoning Mechanismcited by 4
  9. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 4
  10. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematicscited by 4
  11. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generationcited by 1
  12. 2025Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Trainingcited by 1
  13. 2026On Reasoning-Centric LLM-based Automated Theorem Provingcited by 1
  14. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  15. 2026A Task-Centric Theory for Iterative Self-Improvement with Easy-to-Hard Curriculacited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
  2. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  3. 2025Theorem Prover as a Judge for Synthetic Data Generation
  4. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
  5. 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
  6. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
  7. 2025EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving
  8. 2024LeanAgent: Lifelong Learning for Formal Theorem Proving