LeanProgress: Guiding Search for Neural Theorem Proving

via Proof Progress Prediction

Suozhi Huang 1 Peiyang Song 2 Robert Joseph George 2 Anima Anandkumar 2

Abstract 1. Introduction
Mathematical reasoning remains a significant Formal theorem proving (Avigad, 2023) has emerged as a
arXiv:2502.17925v2 [[Link]] 27 Feb 2025

challenge for Large Language Models (LLMs) cornerstone of rigorous mathematical verification, provid-
due to hallucinations. When combined with for- ing machine-checked guarantees for proofs ranging from
mal proof assistants like Lean, these hallucina- foundational results (Gowers et al., 2023) to industrial ap-
tions can be eliminated through rigorous verifica- plications (Community, 2022). The Lean proof assistant
tion, making theorem proving reliable. However, (Moura & Ullrich, 2021), built on dependent type theory, has
even with formal verification, LLMs still strug- witnessed remarkable adoption growth (Best et al., 2023),
gle with long proofs and complex mathematical fueled by collaborative efforts on large-scale formalization
formalizations. While Lean with LLMs offers projects (mathlib Community, 2020) and novel mathemat-
valuable assistance with retrieving lemmas, gen- ical developments (Asgeirsson, 2024). This collaborative
erating tactics, or even complete proofs, it lacks paradigm shift underscores the urgent need for enhanced
a crucial capability: providing a sense of proof tooling to support mathematicians navigating increasingly
progress. This limitation particularly impacts the complex proof environments.
overall development efficiency in large formal-
The recent success of Large Language Models (LLMs) in
ization projects. We introduce LeanProgress, a
code generation (Rozière et al., 2024) and symbolic rea-
method that predicts the progress in the proof.
soning (Yu et al., 2024) has spurred innovations at the in-
Training and evaluating our models made on a
tersection of LLMs and formal verification. Some of the
large corpus of Lean proofs from Lean Workbook
works that have been developed include LeanDojo (Yang
Plus and Mathlib4 and how many steps remain to
et al., 2024b) which provides an interactive environment
complete it, we employ data preprocessing and
for training LLMs on tactic-level interactions while LLM-
balancing techniques to handle the skewed distri-
Step (Welleck & Saha, 2023) and LeanCopilot (Song et al.,
bution of proof lengths. Our experiments show
2024) focuses on next-tactic suggestion through interface as
that LeanProgress achieves an overall prediction
a useful tool. Lean Agent (Kumarappan et al., 2024) then
accuracy of 75.1% in predicting the amount of
combines neural suggestion with life-long learning while
progress and, hence, the remaining number of
Lean Aide (Agrawal et al., 2022) and Lean-STaR(Lin et al.,
steps. When integrated into a best-first search
2024) translates statements written in natural language in
framework using Reprover, our method shows
a doc-string like format to Lean types (including theorem
a 3.8% improvement on Mathlib4 compared to
statements) and bootstrapping thoughts. While these sys-
baseline performances of 41.2%, particularly for
tems demonstrate impressive tactic-level accuracy (Johans-
longer proofs. These results demonstrate how
son, 2023), they primarily optimize for local correctness
proof progress prediction can enhance both auto-
rather than global proof progress – a critical limitation when
mated and interactive theorem proving, enabling
navigating Lean’s vast action space (Nawrocki et al., 2023).
users to make more informed decisions about
proof strategies. Reinforcement learning (RL) presents a theoretically ap-
1 pealing framework for automated theorem proving (Dong
Institute for Interdisciplinary Information Sciences,
Tsinghua University, Beijing, China 2 Computing + Mathe- et al., 2024), where finding reward signals over proof trajec-
matical Sciences Department, California Institute of Tech- tories is essential. However, the combinatorial explosion of
nology, Pasadena, CA, U.S.A.. Correspondence to: Suozhi tactic sequences in Lean (Clune, 2023) renders direct RL
Huang <huang-sz20@[Link]>, Peiyang applications impractical (Setlur et al., 2024). Alphaproof
Song <psong@[Link]>, Robert Joseph George <rge- (AlphaProof & AlphaGeometry, 2024) has done RL for the-
orge@[Link]>, Anima Anandkumar <anima@[Link]>.
orem proving but it’s not open source and needs enormous
compute. Current approaches mitigate this through hybrid

1
 LeanProgress

Proof Tree Data Construction Progress Prediction Integration with LeanCopilot

induction n, rfl
built-in tactic
n:ℕ simp [add, ih] predict_steps
⊢ add 0 n = n Local context
⊢ Goal
Tactic
Induction n

⊢ add 0 0 = 0 n’ : ℕ
ih: add 0 n’ = n’ distribution
rfl
⊢ add 0 (n’+1) = n’+1
remaining steps=3
simp [add, ih]
balancing LLM on
local context local server
+ history
+ number of steps

log prob = 0.4 remaining steps = 1

case n n:ℕ case n

n:ℕ log prob = 0.3 remaining steps = 3
⊢ add 0 n = n ⊢ add 0 n = n

log prob = 0.2 remaining steps = 2

log prob score as critic # remaining steps as signal

Figure 1. The visualization of LeanProgress. LeanProgress is a lightweight framework that collects the number of remaining steps in
proof trees and then balances the data distribution to train the language model. Then LeanProgress takes the proof state as input to generate
the remaining steps for each state as a signal for search. LeanProgress also integrates the tactic predict steps in LeanCopilot as a
user-friendly tool.

architectures (Wang et al., 2023) but remain fundamentally provides a global view of the proof process by predicting
limited by the absence of reliable progress indicators to the remaining steps rather than the immediate next tactic.
guide exploration – a prerequisite for effective RL in mathe-
Progress-Guided Proof Search: We integrate our step pre-
matical domains (Gao et al., 2024).
diction model into a best-first search framework. A natural
We address this critical gap with LeanProgress (Fig 2), a first step for using the progress predictor is combining the
lightweight framework that predicts remaining proof steps predicted remaining steps with the tactic generator’s log
through learned progress signals with search methods be- probabilities to guide the search. In the future, we hope to
yond log-probability based search (Song et al., 2024) or use this, instead of just relying on the log probabilities, as
manual heuristics (Ringer et al., 2021). a reward for RL. We observe on Mathlib4 a significant im-
provement of 3.8% with the baseline Reprover performance
LeanProgress makes the following key contributions:
of 41.2%.
Balanced Data Generation Pipeline: We construct a bal-
Integration with LeanCopilot: Based on the Lean-
anced dataset of approximately 80k proof trajectories from
Copilot framework, we provide a new built-in tactic
Lean Workbook Plus and Mathlib4 by performing a tree
predict steps with suggestion within the stan-
search and selecting the shortest path as ground truth. We
dard Lean user interface. It is a helpful tool that not only
employ a data balancing strategy based on relative proof
suggest tactics but also offer users immediate feedback on
progress. Since the useful and non-trivial data of long proofs
proof progress and potential next steps.
are long-tailed distributed in the original dataset, we fully
utilize long proof data by assigning each state with a remain-
ing step as a label. 2. Related Work
Model for Progress Prediction: We fine-tune a DeepSeek LLMs for Formal Proof Generation. Large Language
Coder V1 1.3b base model to predict the remaining steps, Models (LLMs) have demonstrated significant potential in
achieving a Mean Absolute Error (MAE) of 3.29 and an the field of formal theorem proving (Yang et al., 2024a),
overall prediction accuracy of 75.1% on the test set with finding applications across various proof assistants (Yang
proof history. Unlike tactic suggestion tools, LeanProgress et al., 2024b; Song et al., 2024; Lama et al., 2024). Current

2
 LeanProgress

research on LLM-based theorem proving primarily focuses necessitates effective guiding mechanisms. This highlights
on several key tasks. A prominent application is tactic sug- the need for methods that can provide a global perspective
gestion. Following GPT-f (Polu & Sutskever, 2020), LLMs on proof progress, which our work addresses by predicting
are employed to predict the most promising next tactic given the number of remaining steps.
the current proof state. These methods are often coupled
with proof search algorithms, such as best-first search (Yang 3. Data Generation for LeanProgress
et al., 2024b) or majority voting (Zhou et al., 2024), to ex-
plore the proof space and discover complete proofs (Wu This section details the data generation and processing
et al., 2024). Other techniques, such as retrieval-augmented methodology used to train LeanProgress. We describe the
LLMs (Yang et al., 2024b) and agentic approaches (Thakur process of generating proof trees using best-first search
et al., 2024), provides further aids for tactic generation by (BFS) and the Reprover model, the resulting dataset of proof
selecting relevant lemmas and enabling multi-round proof re- trajectories, and the adjustments made to address the skewed
finement utilizing environment feedback. Moreover, emerg- distribution of proof lengths.
ing research directions include autoformalization (Wu et al.,
2022; Jiang et al., 2023), which aims to translate informal 3.1. Preliminaries: Tactic Prediction as an MDP
mathematical text into formal proofs, and the direct gener-
ation of complete proof sketches (Jiang et al., 2022; Wang Interactive Theorem Provers (ITPs) frame theorem proving
et al., 2024), both of which can be combined with proof as a search problem. As Fig 2 shows, the initial theorem to
generation to enable large-scale training despite inherent be proven represents the initial state, and the application of
proof data scarcity. Our work addresses the gap from local tactics generates transitions to new states, each containing
tactic prediction to a global understanding of the proof tra- subgoals. The objective is to find a sequence of tactics that
jectory by focusing on predicting the number of remaining leads to a state where all subgoals are proven. This search
steps required for proof completion, offering a novel way process is central to automated theorem proving, and our
for new applications of reinforcement learning in automated work focuses on providing valuable information to guide
theorem proving. this search within the Lean ITP.

Interactive Tools for Formal Theorem Proving. Mathe- The theorem-proving problem can be formalized
maticians proving theorems in Lean can significantly benefit as a Markov Decision Process (MDP), denoted as
from interactive tools that integrate seamlessly into the Lean (S, A, Pa , Ra ), where S represents the set of all possible
workflow and provide aids. LLMStep (Welleck & Saha, proof states. A represents the set of all available tactics
2023) extracts current proof states from Lean and sends it (actions). Pa represents the state transition probabilities
to a remote server for LLM-generated tactic suggestions. after executing tactic a in state s. Ra represents the reward
LeanCopilot (Song et al., 2024) improves the user expe- obtained by executing tactic a. From an MDP perspective, a
rience by having fully native tactic suggestion and proof proof process can be viewed as a trajectory of states, tactics,
search tools in Lean, besides an additional functionality and rewards: (si , ai , ri ), where the proof assistant (e.g.,
of premise selection, providing more comprehensive assis- Lean) provides the next state si+1 given the current state si
tance for the proving process. CoqPilot (Kozyrev et al., and the applied tactic ai .
2024), a VS Code extension for Coq, uses LLMs, among In typical tactic prediction, proving a theorem involves pro-
other generative methods, to fill in proof holes by an “ad- viding a proof state s to a language model L, which then
mit” tactic. Unlike these tactics or proof-centric approaches, generates a tactic a, i.e., πL (a|s). Typically, final states
we predict the number of remaining steps by adding a new (where the goal is proven) are assigned a reward of 1, indi-
tactic, predict steps with suggestion based on cating successful completion of the proof.
LeanCopilot, providing tactic suggestions ranked by the
output number of remaining steps as a score. 3.2. Generating Proof Trees and Trajectories
LLM Guidance in Search. Effective proof search is es- A common evaluation strategy for neural theorem provers is
sential for automated theorem proving. While scaling com- best-first search (BFS), as used in GPT-f and related research
putational resources during search has led to significant ad- (Han et al., 2021). This method explores the proof space
vancements, as seen in AlphaGeometry (Trinh et al., 2024) by iteratively expanding the ”best” state, determined by
and AlphaProof (AlphaProof & AlphaGeometry, 2024) for the maximum cumulative log probability of the preceding
IMO problems and in recent work on natural language rea- proof trajectory. Specifically, given a set of unexpanded
soning (Lightman et al., 2023; Yang et al., 2022; Zhang si , the ”best” state to expand is chosen according to:
states P
et al., 2024; Xie et al., 2024) (including OpenAI’s o1, o3 i−1
maxi j=0 log p(aj , sj ), where (s0 , a0 ), . . . , (si−1 , ai−1 )
model (Jaech et al., 2024; Xu et al., 2025)), proof search is is the proof trajectory before state si and log p(aj , sj ) is the
a bit different. The vast search space of possible proof steps average log probability of the generated tokens for the tactic

3
 LeanProgress

Figure 2. The visualization of extract proof tree in theorem proving.

aj in state sj .
Our work utilizes BFS in conjunction with the Reprover D = {(si,j ∗ ,l , ni,j ∗ − l) | ti ∈ T, 1 ≤ l ≤ ni,j ∗ }
model (Yang et al., 2024b) to generate successful proof trees.
By systematically applying Reprover to all reachable states
within a certain depth in a best-first manner, we construct where si,j ∗ ,l is the l-th state in the selected proof trajectory
a tree of successful proofs. This approach allows us to pi,j ∗ for theorem ti , and ni,j ∗ − l represents the number of
collect a dataset of complete proof trajectories, which is then remaining steps from state si,j ∗ ,l to the end of the proof.
used to train our model to predict the number of remaining
steps. This data generation process is crucial for training 3.3. Data Balancing
our model to understand the relationship between proof We evaluated our models on a dataset of Lean proofs ex-
states and the number of steps required for completion. In tracted from Lean Workbook Plus and Mathlib4. The origi-
particular, if multiple proofs are found for a theorem (i.e., nal dataset exhibited a skewed distribution of proof lengths,
multiple no goals nodes are reached), we select the proof with an average proof length of Loriginal = 2.47. This dis-
with the minimum depth (the length of the path from the tribution is shown in Figure 3(a). We adjusted the data
root node to the no goals node) to ensure the quality and distribution based on relative progress within each proof
consistency of the training data. to address this imbalance and ensure a more representative
Formally, let T = {t1 , t2 , ..., tM } be the set of theo- sample of different proof stages.
rems in our dataset. For each theorem ti ∈ T , we per- The adjustment was performed by assigning different sam-
form BFS using the Reprover model to generate a set pling ratios to five ranges of proof lengths: 1-5 steps (Basic
of successful proof trajectories Pi = {pi,1 , pi,2 , ..., pi,ki }, progress, 0.01 ratio), 6-10 steps (Intermediate progress, 0.3
where ki is the number of proofs found for theorem ti . ratio), 11-15 steps (Moderate progress, 0.5 ratio), 16-20
Each proof trajectory pi,j is a sequence of proof states: steps (Advanced progress, 0.7 ratio), and 21+ steps (Expert
pi,j = (si,j,1 , si,j,2 , ..., si,j,ni,j ), where ni,j is the length progress, 1.0 ratio). This strategy effectively upsamples
(number of steps) of the j-th proof for theorem ti . longer proofs and downsamples shorter ones, resulting in a
If ki > 1, we select the proof trajectory pi,j ∗ with the more balanced dataset. The resulting adjusted distribution
minimum depth: has an average proof length of Ladjusted = 10.1, and the
comparison is shown in Figure 3(b).
The dataset was then split into training, validation, and
j ∗ = arg min{ni,j | 1 ≤ j ≤ ki } test sets. The test set contains 88,233 proof states. The
j training set contains Ntrain proof states, and the validation
set contains Nval proof states. The dataset was partitioned
randomly at the theorem level, meaning that all states from
Our training dataset D is then constructed by extracting a given theorem belong to the same split (either training,
(state, remaining steps) pairs from the selected proof trajec- validation, or test). This prevents data leakage between
tories: splits.

4
 LeanProgress

(a) Original dataset of steps distribution (b) Adjusted dataset of steps distribution by balancing different
ranges

Figure 3. Distribution of proof lengths before and after adjustment. Fig (a) shows Original dataset with average proof length of
Loriginal = 2.47. We address the imbalance by assigning each range with different sample ratios. After adjustment the average proof length
of Loriginal = 10.1. This dataset is balanced to keep more long proof paths.

4. Model Training & Experiments representing the remaining steps.

This section describes the experimental setup, including The model was fine-tuned using a Mean Squared Error
model training and results of evaluating LeanProgress’s (MSE) loss function with the AdamW optimizer. The train-
Step Predictor: Prediction accuracy and search pass rate ing was conducted batch size of 4 and a learning rate of
improvement compared to traditional best-first search via 1e − 5. Other parameters are like betas (0.9, 0.999) with
log probability. weight decay 0.01 and warmup ratio 0.03.
We experimented with other models, such as DeepSeek
4.1. Language Model: Remaining Step Predictor coder V2 or Prover V1.5, but the model size of 7B is not
Our approach uses a language model to predict the num- capable of being used on personal computers. We found that
ber of steps remaining to reach a no goals state (proof the DeepSeek Coder 1.3B model provided the best balance
completion) given a current proof state. While the language between performance and computational efficiency.
model architecture can be varied, we employ a fine-tuned
DeepSeek Coder 1.3B model (Guo et al., 2024). This model 4.2. Proof History Utilization
is trained to predict the number of remaining steps based on We investigated the impact of incorporating proof history
the current proof state and, optionally, the history of applied into the input for remaining step prediction. We compared
tactics. the performance of our model when using only the current
The input format for our model is as follows: proof state (state before) as input against using both the
current state and the preceding tactic sequence (state proof).
[STATE BEFORE]state The results, shown in Table 1, demonstrate the importance
[STEPS TO NO GOALS]steps of including proof history. The prompt formats used for
Here, state represents the current proof state, encoded as these two settings are as follows:
a string representing the current goals. The model is trained
to generate the number of remaining steps after this prompt. • state before:
This input format allows the model to focus specifically
on the task of predicting the remaining steps, distinct from
--- STATE_BEFORE: {state_before}
predicting the next tactic.
--- STEPS_TO_NO_GOALS:
We fine-tuned the DeepSeek Coder 1.3B model on (state,
remaining steps) pairs extracted from successful proof tra-
jectories generated using BFS and the Reprover model as • state proof:
described in the previous subsection. The DeepSeek Coder
model was chosen for its strong performance in code under- --- STATE_BEFORE: {state_before}
standing tasks with less than 2B parameters so that personal --- PROOF: {proof}
computers can support inference locally, which we believe --- STEPS_TO_NO_GOALS:
translates well to the task of predicting a numerical value

5
 LeanProgress

Where {state before} represents the current proof Input Range Total Samples Accuracy MAE
state, and {proof} represents the sequence of tactics ap-
plied so far. state 1-5 2.82k 71.1% 1.412
6-10 1.17k 52.1% 2.920
11-15 567 47.7% 6.808
4.3. Evaluation
16-20 563 63.2% 4.915
We evaluate our model in two ways. First, we assess the 21+ 3.70k 59.7% 8.648
accuracy of our step predictions directly on our generated Overall 8.82k 61.8% 5.217
dataset by calculating the Mean Absolute Error (MAE). Sec- proof 1-5 2.82k 79.0% 1.066
ond, we investigate the potential of using our step predic- 6-10 1.17k 61.5% 2.857
tions as a ranking score within a best-first search framework, 11-15 567 68.3% 4.341
comparing its performance against standard best-first search 16-20 563 77.1% 2.748
based solely on log probabilities. 21+ 3.70k 76.7% 5.221
Overall 8.82k 75.1% 3.290
4.3.1. MAE E VALUATION ON S TEPS DATASET
To evaluate the accuracy of our step predictions, we cal- Table 1. Comparison of MAE and Accuracy with and without
culate the Mean Absolute Error (MAE) on our generated Proof History.
dataset D. Given a state si,j ∗ ,l in the selected proof tra-
jectory for theorem ti , our model predicts the number of
remaining steps as n̂i,j ∗ ,l = f (si,j ∗ ,l ). The actual number 4.3.3. C OMBINING B EST-F IRST S EARCH WITH S TEPS
of remaining stepsPis ni,j ∗ − l. The MAE is then calculated P REDICTION
1
as: MAE = |D| (s,n)∈D |n̂ − n| where |D| is the total
Beyond direct prediction accuracy, we explore the potential
number of (state, remaining steps) pairs in our dataset. This
of using our step predictions to guide proof search. We
metric provides a direct measure of the average difference
integrate our model into a best-first search framework by
between our model’s predictions and the true number of
combining the predicted remaining steps with the log proba-
remaining steps.
bilities of the tactic sequence. Specifically, when selecting
4.3.2. P ROOF H ISTORY H ELPS S TEP P REDICTION the next state to expand, insteadPof using only the cumu-
i−1
lative log probability L(si ) = j=0 log p(aj |sj ), where
We evaluate the prediction accuracy using Mean Absolute (s0 , a0 ), . . . , (si−1 , ai−1 ) is the proof trajectory before state
Error (MAE), which measures the average absolute differ- si and log p(aj |sj ) is the average log probability of the
ence between the predicted number of remaining steps and generated tokens for the tactic aj given state sj , we use a
the actual number of remaining steps. A lower MAE indi- combined score: C(si ) = αN (si ) + (1 − α)P (si ), where
cates better prediction accuracy. Table 1 presents the MAE α ∈ [0, 1] is a hyperparameter that controls the relative
and accuracy results for both input formats across differ- importance of the normalized steps N (si ) and the log prob-
ent ranges of proof lengths and overall. The table shows ability P (si ).
the total number of samples for each range, along with the
The normalized steps are calculated as N (si ) =
accuracy and MAE achieved by each input format.
−2n̂i /Nmax , where n̂i = f (si ) is the predicted number
From the results in Table 1, we observe a significant perfor- of remaining steps for state si , and Nmax is the maximum
mance drop when only the input state is used (state before). possible number of steps from all states in a proof.
Including all previous tactics in the prompt (state proof)
We compare the performance of this combined ap-
provides a ”direction” for the proof, leading to better perfor-
proach(where α = 0.2) with a standard best-first search
mance and more accurate predictions, as evidenced by the
using only log probabilities (equivalent to setting α = 0).
consistently lower MAE values across all ranges and overall.
We evaluate both approaches by measuring the number of
This improvement is likely due to the fact that proof history
theorems solved within a fixed number of expansions and
encodes information beyond the current state, such as con-
the average number of expansions required to find a proof.
sistent application of specific mathematical techniques (e.g.,
This comparison demonstrates the effectiveness of incorpo-
repeated use of exponentiation or logarithms) or the over-
rating our step predictions into the search process.
all strategy being employed. This contextual information
allows the model to make more informed predictions about Proof search requires a search algorithm and a method for
the remaining steps. interacting with Lean. So, we chose the best-first search for
LeanDojo’s implementation. Best-first search is parameter-
ized by the maximum number of generated tactics, defined
as the number of attempts × expansion size per iteration

6
 LeanProgress

Input (User) theorem

theorem lean_workbook_plus_74374 (m n : N) : (m * n +
m + n) % 6 = 4 → 12 | m * n := by

predict steps with suggestion

Suggestion (LeanProgress) Lean Infoview
Try these:

• rw [[Link] comm]
• intro h

• rw [← [Link] add div m n]

• rw [[Link] iff mod eq zero]
• omega

Steps remaining: 6

Figure 4. Simulated example showing the use of predict steps with suggestion. The tactic predicts 6 remaining steps and
suggests 5 tactics. The first 3 tactics for this proof should be intro h, have g := congr arg (· % 6) h and simp at g.

× maximum iterations, subject to a timeout. We use a 2- LeanCopilot provides a general framework of develop-
minute timeout and use beam search with a size of 1 × 32 ing LLM-based tools natively in Lean, and supports a
due to memory constraints. suggest tactic functionality that offers tactic sugges-
tions, it lacks concrete feedback to help users choose among
We compare our method, which combines predicted remain-
tactic candidates, which creates inefficiency due to repetitive
ing steps with log probabilities, against standard best-first
trial-and-error during the theorem proving process. With
search using only log probabilities. We evaluate the Le-
each tactic candidate, LeanCopilot only offers the resulting
anDojo v4 test dataset. The primary metric for evaluating
state if applying that tactic, together with a log probabil-
proof search performance is the percentage of theorems
ity score from the tactic generation model. While the log
solved within the timeout.
probability score hard to concretize and the resulting state
The results of this comparison are shown in Table 2, which oftentimes too complicated to interpret directly, using pre-
demonstrate the effectiveness of incorporating our step pre- diction of numbers of remaining steps helps guide users
dictions into the proof search process. directly and concretely in choosing tactics.
Thus, to complement existing tactic suggestion, we leverage
Method Mathlib4-test LeanCopilot’s neural network inference framework in Lean,
Original LogP 41.2% and builds a practical tool upon suggest tactic that
Steps as Critic 45.0% additionally shows the number of remaining steps from each
tactic candidate. The whole functionality is wrapped into a
Table 2. Comparison of Proof Search Performance: Pass rates on single tactic predict steps with suggestion that
the Mathlib4-test dataset with Lean. This table shows the pass is directly usable within a standard Lean workflow.
rates of previous logP method and ours. In sampling, we used a
model with a temperature of 0.7; we sampled 32 examples once.

Case Study for Tool Use. To further illustrate the practical

5. Practical Tool Development & Qualitative application and effectiveness of LeanProgress, we present
Examples a case study demonstrating its use within the LeanCopilot
environment. This example showcases how the combined
Practical Tool Development. With the Step Predictor, display of tactic suggestions and remaining step predictions
one immediate practical application is to couple with tactic can aid users in navigating complex proofs, particularly in
suggestion and offer indications of proof progress. While number theory.

7
 LeanProgress

Figure 4 (simulated) demonstrates LeanProgress’s assis- LeanProgress with reinforcement learning (RL) techniques.
tance in proving a divisibility theorem. The user begins LeanProgress’s ability to predict the number of remaining
with the goal of proving that if (m ∗ n + m + n) mod steps in a proof can provide a continuous and informative
6 = 4 for natural numbers m and n, then 12 divides reward signal for RL agents. Unlike binary rewards that
m ∗ n (written as 12 | (m ∗ n) in Lean). The user only indicate success or failure at the end of a proof at-
inputs the theorem statement into Lean and invokes the tempt, this continuous feedback allows the agent to learn
predict steps with suggestion command. The from partial progress throughout the proving process. They
Lean Infoview then displays the following information, of- could also learn more efficiently by receiving meaningful
fering both a prediction of the remaining proof steps and a feedback throughout the proving process while developing
set of suggested tactics. better long-term strategies for complex proofs. This could
then enable the model to adapt its behavior based on the
Case Study for Proof Guided by LeanProgress. We difficulty and progress of the current theorem and achieve
now analyze a specific example, mathd algebra 296, higher success rates on challenging theorems that require
to illustrate the advantage of using Progress Predictor. The many steps.
theorem and proof is:
3) Lightweight and Scalable Implementations: Future
theorem mathd_algebra_296 : abs (((3491 - work could also focus on developing more lightweight im-
60) * (3491 + 60) - 3491ˆ2):Z) = 3600
plementations of LeanProgress. This could involve explor-
:= by
rw abs_of_nonpos ing model compression techniques or developing more effi-
norm_num cient architectures that maintain prediction accuracy while
norm_num reducing computational requirements. Such improvements
would make LeanProgress more accessible and easier to
This theorem was successfully proven with the aid of our integrate into existing theorem-proving workflows.
Progress Predictor. A key observation is that a naive applica-
tion of norm num would not suffice to complete the proof.
The Progress Predictor leverages the recorded proof history
7. Conclusion
and inferred the application of the difference of squares We introduce LeanProgress, a approach to enhance interac-
factorization. By leveraging proof history and remaining tive theorem proving in Lean by integrating a remaining step
steps, the Progress Predictor likely guided the prover to predictor into the LeanCopilot frontend. Our work makes
apply norm num multiple times, ultimately leading to the several significant contributions to the field of automated
successful derivation of the target value. A standard Re- theorem proving. We developed a method for generating a
prover, lacking access to the proof history, would struggle balanced dataset of proof trajectories by adjusting the sam-
with this theorem. pling ratio based on proof length, addressing the challenge
of skewed distributions in proof complexity. We then trained
6. Limitations and Future Work a remaining step prediction model using a novel input for-
mat that incorporates the current proof state and, optionally,
LeanProgress represents a significant advancement in guid- the proof history. Integrating this model into the LeanCopi-
ing search for neural theorem proving through proof lot interface provides users with both tactic suggestions and
progress prediction. However, it is important to note that remaining step predictions, offering a more comprehensive
this work is just the first step in a broader research agenda. tool for guiding the proof process. Our results highlight
There are several promising avenues for future work that the potential of proof progress prediction in enhancing both
could further enhance the capabilities and applications of automated and interactive theorem proving, enabling users
LeanProgress. to make more informed decisions about proof strategies.
1) Incorporating Tree-of-Thought and Chain-of- Lastly, LeanProgress represents a significant step forward in
Thought Approaches: One potential direction for bridging the gap between local tactic prediction and global
future research is to integrate tree-of-thought (ToT) and proof trajectory understanding, opening up new possibilities
chain-of-thought (CoT) methodologies into LeanProgress. for the application of reinforcement learning in automated
These approaches could provide a more structured and theorem proving and paving the way for more efficient and
interpretable way of reasoning about proof progress. By effective proof development in large formalization projects.
incorporating ToT and CoT, we could potentially improve
the model’s ability to explain its predictions and provide 8. Impact Statement
more detailed insights into the proof process.
This paper presents work whose goal is to advance the field
2) Integration with Reinforcement Learning: A particu- of machine learning and interactive theorem proving. There
larly promising avenue for future work is the integration of

8
 LeanProgress

are many potential societal consequences of our work, none Gao, J., Xu, S., Ye, W., Liu, W., He, C., Fu, W., Mei,
which we feel must be specifically highlighted here. Z., Wang, G., and Wu, Y. On designing effective rl
reward at training time for llm reasoning, 2024. URL
References [Link]

Agrawal, A., Gadgil, S., Goyal, N., Narayanan, A., and Gowers, W. T., Green, B., Manners, F., and Tao, T. On a
Tadipatri, A. Towards a mathematics formalisation assis- conjecture of marton, 2023. URL [Link]
tant using large language models, 2022. URL https: org/abs/2311.05762.
//[Link]/abs/2211.07524.
Guo, D., Zhu, Q., Yang, D., Xie, Z., Dong, K., Zhang,
AlphaProof, T. and AlphaGeometry, T. Ai achieves silver- W., Chen, G., Bi, X., Wu, Y., Li, Y., Luo, F., Xiong,
medal standard solving international 178 mathematical Y., and Liang, W. Deepseek-coder: When the large lan-
olympiad problems. DeepMind blog, 179, 2024. guage model meets programming – the rise of code in-
telligence, 2024. URL [Link]
Asgeirsson, D. Towards Solid Abelian Groups: A Formal 2401.14196.
Proof of Nöbeling’s Theorem. In Bertot, Y., Kutsia, T.,
and Norrish, M. (eds.), 15th International Conference Han, J. M., Rute, J., Wu, Y., Ayers, E. W., and Polu, S. Proof
on Interactive Theorem Proving (ITP 2024), volume artifact co-training for theorem proving with language
309 of Leibniz International Proceedings in Informatics models. arXiv preprint arXiv:2102.06203, 2021.
(LIPIcs), pp. 6:1–6:17, Dagstuhl, Germany, 2024. Schloss
Dagstuhl – Leibniz-Zentrum für Informatik. ISBN 978- Jaech, A., Kalai, A., Lerer, A., Richardson, A., El-Kishky,
3-95977-337-9. doi: 10.4230/[Link].2024.6. URL A., Low, A., Helyar, A., Madry, A., Beutel, A., Car-
[Link] ney, A., et al. Openai o1 system card. arXiv preprint
document/10.4230/[Link].2024.6. arXiv:2412.16720, 2024.
Avigad, J. Mathematics and the formal turn, 2023. URL Jiang, A. Q., Welleck, S., Zhou, J. P., Li, W., Liu, J., Jamnik,
[Link] M., Lacroix, T., Wu, Y., and Lample, G. Draft, sketch,
Best, A. J., Birkbeck, C., Brasca, R., and Rodriguez Boidi, and prove: Guiding formal theorem provers with informal
E. Fermat’s Last Theorem for Regular Primes. proofs. arXiv preprint arXiv:2210.12283, 2022.
In Naumowicz, A. and Thiemann, R. (eds.), 14th
Jiang, A. Q., Li, W., and Jamnik, M. Multilingual mathemat-
International Conference on Interactive Theorem
ical autoformalization. arXiv preprint arXiv:2311.03755,
Proving (ITP 2023), volume 268 of Leibniz Inter-
2023.
national Proceedings in Informatics (LIPIcs), pp.
36:1–36:8, Dagstuhl, Germany, 2023. Schloss Dagstuhl
Johansson, M. What can large language models do for
– Leibniz-Zentrum für Informatik. ISBN 978-3-
theorem proving and formal methods? In Bridging the
95977-284-6. doi: 10.4230/[Link].2023.36. URL
Gap Between AI and Reality: First International Con-
[Link]
ference, AISoLA 2023, Crete, Greece, October 23–28,
document/10.4230/[Link].2023.36.
2023, Proceedings, pp. 391–394, Berlin, Heidelberg,
Clune, J. A formalized reduction of keller’s conjecture. In 2023. Springer-Verlag. ISBN 978-3-031-46001-2. doi:
Proceedings of the 12th ACM SIGPLAN International 10.1007/978-3-031-46002-9 25. URL [Link]
Conference on Certified Programs and Proofs, CPP 2023, org/10.1007/978-3-031-46002-9_25.
pp. 90–101, New York, NY, USA, 2023. Association for
Computing Machinery. ISBN 9798400700262. doi: 10. Kozyrev, A., Solovev, G., Khramov, N., and Podkopaev,
1145/3573105.3575669. URL [Link] A. Coqpilot, a plugin for llm-based generation of
10.1145/3573105.3575669. proofs. In Proceedings of the 39th IEEE/ACM Inter-
national Conference on Automated Software Engineer-
Community, M. Completion of the liquid tensor ex- ing, ASE ’24, pp. 2382–2385. ACM, October 2024. doi:
periment. [Link] 10.1145/3691620.3695357. URL [Link]
[Link]/blog/posts/lte-final/, 2022. org/10.1145/3691620.3695357.

Dong, K., Mahankali, A., and Ma, T. Formal theorem Kumarappan, A., Tiwari, M., Song, P., George, R. J., Xiao,
proving by rewarding llms to decompose proofs hier- C., and Anandkumar, A. Leanagent: Lifelong learning for
archically, 2024. URL [Link] formal theorem proving, 2024. URL [Link]
2411.01829. org/abs/2410.06209.

9
 LeanProgress

Lama, V., Ma, C., and Ghosal, T. Benchmarking auto- N., Scialom, T., and Synnaeve, G. Code llama: Open
mated theorem proving with large language models. In foundation models for code, 2024. URL https://
Proceedings of the 1st Workshop on NLP for Science [Link]/abs/2308.12950.
(NLP4Science), pp. 208–218, 2024.
Setlur, A., Nagpal, C., Fisch, A., Geng, X., Eisenstein, J.,
Lightman, H., Kosaraju, V., Burda, Y., Edwards, H., Baker, Agarwal, R., Agarwal, A., Berant, J., and Kumar, A.
B., Lee, T., Leike, J., Schulman, J., Sutskever, I., and Rewarding progress: Scaling automated process verifiers
Cobbe, K. Let’s verify step by step. arXiv preprint for llm reasoning, 2024. URL [Link]
arXiv:2305.20050, 2023. abs/2410.08146.
Lin, H., Sun, Z., Yang, Y., and Welleck, S. Lean-star: Song, P., Yang, K., and Anandkumar, A. Towards large
Learning to interleave thinking and proving, 2024. URL language models as copilots for theorem proving in
[Link] lean, 2024. URL [Link]
12534.
mathlib Community, T. The lean mathematical library. In
Proceedings of the 9th ACM SIGPLAN International Thakur, A., Tsoukalas, G., Wen, Y., Xin, J., and Chaud-
Conference on Certified Programs and Proofs, CPP huri, S. An in-context learning agent for formal theorem-
2020, pp. 367–381, New York, NY, USA, 2020. Associa- proving, 2024. URL [Link]
tion for Computing Machinery. ISBN 9781450370974. 2310.04353.
doi: 10.1145/3372885.3373824. URL [Link]
org/10.1145/3372885.3373824. Trinh, T. H., Wu, Y., Le, Q. V., He, H., and Luong, T. Solv-
ing olympiad geometry without human demonstrations.
Moura, L. d. and Ullrich, S. The lean 4 theorem prover Nature, 625(7995):476–482, 2024.
and programming language. In Automated Deduction –
CADE 28: 28th International Conference on Automated Wang, H., Xin, H., Zheng, C., Li, L., Liu, Z., Cao, Q.,
Deduction, Virtual Event, July 12–15, 2021, Proceed- Huang, Y., Xiong, J., Shi, H., Xie, E., Yin, J., Li, Z., Liao,
ings, pp. 625–635, Berlin, Heidelberg, 2021. Springer- H., and Liang, X. Lego-prover: Neural theorem proving
Verlag. ISBN 978-3-030-79875-8. doi: 10.1007/ with growing libraries, 2023. URL [Link]
978-3-030-79876-5 37. URL [Link] org/abs/2310.00656.
10.1007/978-3-030-79876-5_37.
Wang, H., Xin, H., Liu, Z., Li, W., Huang, Y., Lu, J., Yang,
Nawrocki, W., Ayers, E. W., and Ebner, G. An Extensible Z., Tang, J., Yin, J., Li, Z., et al. Proving theorems
User Interface for Lean 4. In Naumowicz, A. and Thie- recursively. arXiv preprint arXiv:2405.14414, 2024.
mann, R. (eds.), 14th International Conference on Interac-
tive Theorem Proving (ITP 2023), volume 268 of Leibniz Welleck, S. and Saha, R. Llmstep: Llm proofstep sugges-
International Proceedings in Informatics (LIPIcs), tions in lean. arXiv preprint arXiv:2310.18457, 2023.
pp. 24:1–24:20, Dagstuhl, Germany, 2023. Schloss
Dagstuhl – Leibniz-Zentrum für Informatik. ISBN 978- Wu, Y., Jiang, A. Q., Li, W., Rabe, M., Staats, C., Jam-
3-95977-284-6. doi: 10.4230/[Link].2023.24. URL nik, M., and Szegedy, C. Autoformalization with large
[Link] language models. Advances in Neural Information Pro-
document/10.4230/[Link].2023.24. cessing Systems, 35:32353–32368, 2022.

Polu, S. and Sutskever, I. Generative language model- Wu, Y., Sun, Z., Li, S., Welleck, S., and Yang, Y. Infer-
ing for automated theorem proving. arXiv preprint ence scaling laws: An empirical analysis of compute-
arXiv:2009.03393, 2020. optimal inference for problem-solving with language
models. arXiv preprint arXiv:2408.00724, 2024.
Ringer, T., Porter, R., Yazdani, N., Leo, J., and Grossman,
D. Proof repair across type equivalences. In Proceedings Xie, Y., Goyal, A., Zheng, W., Kan, M.-Y., Lillicrap, T. P.,
of the 42nd ACM SIGPLAN International Conference on Kawaguchi, K., and Shieh, M. Monte carlo tree search
Programming Language Design and Implementation, pp. boosts reasoning via iterative preference learning. arXiv
112–127, 2021. preprint arXiv:2405.00451, 2024.

Rozière, B., Gehring, J., Gloeckle, F., Sootla, S., Gat, I., Xu, F., Hao, Q., Zong, Z., Wang, J., Zhang, Y., Wang,
Tan, X. E., Adi, Y., Liu, J., Sauvestre, R., Remez, T., J., Lan, X., Gong, J., Ouyang, T., Meng, F., et al. To-
Rapin, J., Kozhevnikov, A., Evtimov, I., Bitton, J., Bhatt, wards large reasoning models: A survey of reinforced
M., Ferrer, C. C., Grattafiori, A., Xiong, W., Défossez, reasoning with large language models. arXiv preprint
A., Copet, J., Azhar, F., Touvron, H., Martin, L., Usunier, arXiv:2501.09686, 2025.

10
 LeanProgress

Yang, K., Deng, J., and Chen, D. Generating natural lan-

guage proofs with verifier-guided search. arXiv preprint
arXiv:2205.12443, 2022.
Yang, K., Poesia, G., He, J., Li, W., Lauter, K., Chaudhuri,
S., and Song, D. Formal mathematical reasoning: A new
frontier in ai, 2024a. URL [Link]
abs/2412.16075.

Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P.,
Yu, S., Godil, S., Prenger, R. J., and Anandkumar, A.
Leandojo: Theorem proving with retrieval-augmented
language models. Advances in Neural Information Pro-
cessing Systems, 36, 2024b.

Yu, F., Zhang, H., Tiwari, P., and Wang, B. Natural language
reasoning, a survey. ACM Computing Surveys, 56(12):
1–39, 2024.
Zhang, D., Zhoubian, S., Hu, Z., Yue, Y., Dong, Y., and
Tang, J. Rest-mcts*: Llm self-training via process reward
guided tree search. arXiv preprint arXiv:2406.03816,
2024.
Zhou, J. P., Staats, C., Li, W., Szegedy, C., Weinberger,
K. Q., and Wu, Y. Don’t trust: Verify–grounding llm
quantitative reasoning with autoformalization. arXiv
preprint arXiv:2403.18120, 2024.

11
 LeanProgress

A. Code & Artifacts

We open source all code and artifacts with this work. The complete codebase of data generation pipeline, data processing,
tool development based on LeanCopilot, and main algorithm will be shared in a Github repository, which, together with the
curated dataset, will be made public upon acceptance of this work. For this submission, in respect to the double blind policy,
we submit the complete code in supplementary materials.

B. Qualitative Examples
Complementing case studies in Section 5, we show below more examples of utilizing our Step Predictor alone natively in
Lean, with accurate prediction results.

Figure 5. Qualitative Example 1/6 of running our Step Predictor on real-world Lean problems.

Figure 6. Qualitative Example 2/6 of running our Step Predictor on real-world Lean problems.

Figure 7. Qualitative Example 3/6 of running our Step Predictor on real-world Lean problems.

12
 LeanProgress

Figure 8. Qualitative Example 4/6 of running our Step Predictor on real-world Lean problems.

Figure 9. Qualitative Example 5/6 of running our Step Predictor on real-world Lean problems.

Figure 10. Qualitative Example 6/6 of running our Step Predictor on real-world Lean problems.

13