# LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

arXiv: https://arxiv.org/abs/2502.17925 · HTML: https://mlsanity.com/paper/2502.17925/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 29 of its 43 references that are in the map.
- First posted on arXiv 25 Feb 2025.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 29 of 29)

- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence](https://mlsanity.com/paper/2401.14196/) (2024)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [ReST-MCTS*: LLM Self-Training via Process Reward Guided Tree Search](https://mlsanity.com/paper/2406.03816/) (2024)
- [Towards Large Reasoning Models: A Survey of Reinforced Reasoning with Large Language Models](https://mlsanity.com/paper/2501.09686/) (2025)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Rewarding Progress: Scaling Automated Process Verifiers for LLM Reasoning](https://mlsanity.com/paper/2410.08146/) (2024)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [Monte Carlo Tree Search Boosts Reasoning via Iterative Preference Learning](https://mlsanity.com/paper/2405.00451/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [On Designing Effective RL Reward at Training Time for LLM Reasoning](https://mlsanity.com/paper/2410.15115/) (2024)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Natural Language Reasoning, A Survey](https://mlsanity.com/paper/2303.14725/) (2023)
- [Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization](https://mlsanity.com/paper/2403.18120/) (2024)
- [Generating Natural Language Proofs with Verifier-Guided Search](https://mlsanity.com/paper/2205.12443/) (2022)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [LLMSTEP: LLM proofstep suggestions in Lean](https://mlsanity.com/paper/2310.18457/) (2023)
- [Proving Theorems Recursively](https://mlsanity.com/paper/2405.14414/) (2024)
- [Towards a Mathematics Formalisation Assistant using Large Language Models](https://mlsanity.com/paper/2211.07524/) (2022)
- [Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically](https://mlsanity.com/paper/2411.01829/) (2024)
- [CoqPilot, a plugin for LLM-based generation of proofs](https://mlsanity.com/paper/2410.19605/) (2024)
- [Proof Repair across Type Equivalences](https://mlsanity.com/paper/2010.00774/) (2020)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [Towards solid abelian groups: A formal proof of N"obeling's theorem](https://mlsanity.com/paper/2309.07252/) (2023)

## Built on by (most cited first, 10 of 10)

- [Adaptation of Agentic AI: A Survey of Post-Training, Memory, and Skills](https://mlsanity.com/paper/2512.16301/) (2025)
- [Large Language Model Reasoning Failures](https://mlsanity.com/paper/2602.06176/) (2026)
- [Steer2Adapt: Dynamically Composing Steering Vectors Elicits Efficient Adaptation of LLMs](https://mlsanity.com/paper/2602.07276/) (2026)
- [Interactive Evaluation Requires a Design Science](https://mlsanity.com/paper/2605.17829/) (2026)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)
- [Automating Formal Verification with Reinforcement Learning and Recursive Inference](https://mlsanity.com/paper/2605.30914/) (2026)
- [Real-Time Progress Prediction in Reasoning Language Models](https://mlsanity.com/paper/2506.23274/) (2025)
- [Human agency in initial human-AI proof formalization workflows](https://mlsanity.com/paper/2606.04273/) (2026)
- [Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving](https://mlsanity.com/paper/2608.18084/) (2026)
- [Predicting the Next State Is Not Enough: JEPA Representations for Lean Theorem Proving](https://mlsanity.com/paper/2609.32908/) (2026)

## Abstract (arXiv)

Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucinations can be eliminated through rigorous verification, making theorem proving reliable. However, even with formal verification, LLMs still struggle with long proofs and complex mathematical formalizations. While Lean with LLMs offers valuable assistance with retrieving lemmas, generating tactics, or even complete proofs, it lacks a crucial capability: providing a sense of proof progress. This limitation particularly impacts the overall development efficiency in large formalization projects. We introduce LeanProgress, a method that predicts the progress in the proof. Training and evaluating our models made on a large corpus of Lean proofs from Lean Workbook Plus and Mathlib4 and how many steps remain to complete it, we employ data preprocessing and balancing techniques to handle the skewed distribution of proof lengths. Our experiments show that LeanProgress achieves an overall prediction accuracy of 75.8% in predicting the amount of progress and, hence, the remaining number of steps. When integrated into a best-first search framework using Reprover, our method shows a 3.8% improvement on Mathlib4 compared to baseline performances of 41.4%, particularly for longer proofs. These results demonstrate how proof progress prediction can enhance both automated and interactive theorem proving, enabling users to make more informed decisions about proof strategies. Our code is merged in this library here https://github.com/lean-dojo/LeanDojo-v2.