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

🚩News: Our work is accepted to the Transactions on Machine Learning Research (TMLR).

This is the official codebase accompanying the paper "LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction"), for predicting proof progress in the Lean theorem prover and using that signal to guide neural theorem proving search.

The repository contains scripts to build Lean proof datasets with different step distributions (create_datesets/), model definitions for progress prediction (models/), and simple training and evaluation utilities for large language models (utils/). It is intended as a minimal, research-oriented implementation rather than a polished library. For an introduction and overview, please refer to our webpage; for conceptual details, experimental settings, and full results, please refer to the paper.

Getting in Touch

• For general questions and discussions, please use GitHub Discussions.
• To report a potential bug, please open an issue. In the issue, please include your system information, the exact steps to reproduce the error, and complete logs preferrably in debug mode. Important: If your issue cannot be reproduced easily, it will be unlikely to receive help.
• Feature requests and contributions are warmly welcomed. Please feel free to start a discussion or open a pull request.

Citation

If you find our work useful, please consider citing our paper:

@article{huang2025leanprogress,
  title={LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction},
  author={Huang, Suozhi and Song, Peiyang and George, Robert Joseph and Anandkumar, Anima},
  journal={arXiv preprint arXiv:2502.17925},
  year={2025}
}