mlsanityData to 7 Oct 2026

Lean-STaR: Learning to Interleave Thinking and Proving

arXiv 2407.10040 ↗First posted 14 Jul 2024cs.AIcited by 64

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

Traditional language model-based theorem proving assumes that by training on a sufficient amount of formal proof data, a model will learn to prove theorems. Our key observation is that a wealth of informal information that is not present in formal proofs can be useful for learning to prove theorems. For instance, humans think through steps of a proof, but this thought process is not visible in the resulting code. We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof, thereby boosting the model's theorem-proving capabilities. Lean-STaR uses retrospective ground-truth tactics to generate synthetic thoughts for training the language model. At inference time, the trained model directly generates the thoughts prior to the prediction of the tactics in each proof step. Building on the self-taught reasoner framework, we then apply expert iteration to further fine-tune the model on the correct proofs it samples and verifies using the Lean solver. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment, significantly outperforming base models (boldsymbol43.4% rightarrow 46.3%, Pass@64). We also analyze the impact of the augmented thoughts on various aspects of the theorem proving process, providing insights into their effectiveness.

Key facts. Cited by 64 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 33 of its 61 references that are in the map. First posted on arXiv 14 Jul 2024.

Builds on

33 of 61 references.

Closest ancestors · 4

Same direction, newest first

  1. 2024Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization26 Mar
  2. 2024MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data14 Feb
  3. 2023Llemma: An Open Language Model For Mathematics16 Oct
  4. 2020Generative Language Modeling for Automated Theorem Proving7 Sep

Other references · 29

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2023GPT-4 Technical Reportcited by 18,132
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  4. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  5. 2022Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Taskscited by 1,057
  6. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 895
  7. 2021Show Your Work: Scratchpads for Intermediate Computation with Language Modelscited by 871
  8. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  9. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  10. 2023Beyond Human Data: Scaling Self-Training for Problem-Solving with Language Modelscited by 325
  11. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  12. 2022Autoformalization with Large Language Modelscited by 252
17 more
  1. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 245
  2. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  3. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  4. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  6. 2019The Lean mathematical librarycited by 127
  7. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  8. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  9. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  10. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  11. 2022NaturalProver: Grounded Mathematical Proof Generation with Language Modelscited by 72
  12. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  13. 2019Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizarcited by 40
  14. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  15. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  16. 2022Towards a Mathematics Formalisation Assistant using Large Language Modelscited by 22
  17. 2020Document-Level Definition Detection in Scholarly Documents: Existing Models, Error Analyses, and Future Directionscited by 11

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 11; 2025: 35; 2026: 18.

64 papers.

Sort:

By area:

  1. 2025Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Modelscited by 381
  2. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  4. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  5. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Provingcited by 82
  6. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  7. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  8. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  9. 2025OdysseyBench: Evaluating LLM Agents on Long-Horizon Complex Office Application Workflowscited by 54
  10. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  11. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  12. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
38 more
  1. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  2. 2025Optimizing Temperature for Language Models with Multi-Sample Inferencecited by 33
  3. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 32
  4. 2025Chain-of-Reasoning: Towards Unified Mathematical Reasoning in Large Language Models via a Multi-Paradigm Perspectivecited by 29
  5. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  6. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  7. 2025MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Provingcited by 24
  8. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  9. 2025Learning to Reason via Mixture-of-Thought for Logical Reasoningcited by 20
  10. 2026Large Language Model Reasoning Failurescited by 20
  11. 2025One Example Shown, Many Concepts Known! Counterexample-Driven Conceptual Reasoning in Mathematical LLMscited by 12
  12. 2024SubgoalXL: Subgoal-based Expert Learning for Theorem Provingcited by 11
  13. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  14. 2024What makes math problems hard for reinforcement learning: a case studycited by 9
  15. 2024dafny-annotator: AI-Assisted Verification of Dafny Programscited by 8
  16. 2025From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systemscited by 8
  17. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  18. 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinementcited by 7
  19. 2025AdaSTaR: Adaptive Data Sampling for Training Self-Taught Reasonerscited by 6
  20. 2025Atomic Thinking of LLMs: Decoupling and Exploring Mathematical Reasoning Abilitiescited by 6
  21. 2024YuLan-Mini: An Open Data-efficient Language Modelcited by 5
  22. 2025FANS -- Formal Answer Selection for Natural Language Math Reasoning Using Lean4cited by 5
  23. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  24. 2025GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Provingcited by 5
  25. 2026TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?cited by 5
  26. 2024RL-STaR: Theoretical Analysis of Reinforcement Learning Frameworks for Self-Taught Reasonercited by 4
  27. 2025Steering LLMs for Formal Theorem Provingcited by 4
  28. 2024Proof Flow: Preliminary Study on Generative Flow Network Language Model Tuning for Formal Reasoningcited by 3
  29. 2025Agentic-R1: Distilled Dual-Strategy Reasoningcited by 3
  30. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3
  31. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3
  32. 2026Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repaircited by 3
  33. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 3
  34. 2025Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solvingcited by 2
  35. 2025Can Large Reasoning Models Improve Accuracy on Mathematical Tasks Using Flawed Thinking?cited by 2
  36. 2026Learning to Reason with Insight for Informal Theorem Provingcited by 2
  37. 2025CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimizationcited by 1
  38. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generationcited by 1

50 most cited of 64 All 64 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction
  2. 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations
  3. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
  4. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
  5. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
  6. 2024LeanReasoner: Boosting Complex Logical Reasoning with Lean
  7. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  8. 2025Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework