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.1\% 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.2\%, 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.

翻译：数学推理因幻觉问题仍然是大型语言模型（LLM）面临的重大挑战。当与Lean等形式化证明助手结合时，这些幻觉可通过严格验证消除，从而使定理证明变得可靠。然而，即使具备形式化验证能力，LLM在处理长证明和复杂数学形式化时仍存在困难。虽然结合Lean的LLM在引理检索、策略生成乃至完整证明生成方面能提供有效辅助，但其缺乏一项关键能力：提供证明进度感知。这一局限尤其影响大型形式化项目的整体开发效率。本文提出LeanProgress方法，用于预测证明进度。基于Lean Workbook Plus和Mathlib4的大型Lean证明语料库，我们通过数据预处理和平衡技术处理证明长度分布偏斜问题，训练并评估了预测剩余证明步数的模型。实验表明，LeanProgress在进度量预测（即剩余步数预测）中达到75.1%的整体准确率。当集成至使用Reprover的最佳优先搜索框架时，本方法在Mathlib4上相比41.2%的基线性能提升3.8%，在长证明场景中提升尤为显著。这些结果表明证明进度预测能够增强自动化和交互式定理证明能力，帮助用户制定更具洞察力的证明策略。