# Machine-Learned Premise Selection for Lean

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

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 16 references that are in the map.
- First posted on arXiv 17 Mar 2023.

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

- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021)

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

- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [Rigor with Machine Learning from Field Theory to the Poincar'e Conjecture](https://mlsanity.com/paper/2402.13321/) (2024)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [Premise Selection for a Lean Hammer](https://mlsanity.com/paper/2506.07477/) (2025)
- [Neuro-Symbolic Proof Generation for Scaling Systems Software Verification](https://mlsanity.com/paper/2603.19715/) (2026)
- [Beyond Correctness: Toward Automated Novelty Verification with Lean 4](https://mlsanity.com/paper/2608.14669/) (2026)

## Abstract (arXiv)

We introduce a machine-learning-based tool for the Lean proof assistant that suggests relevant premises for theorems being proved by a user. The design principles for the tool are (1) tight integration with the proof assistant, (2) ease of use and installation, (3) a lightweight and fast approach. For this purpose, we designed a custom version of the random forest model, trained in an online fashion. It is implemented directly in Lean, which was possible thanks to the rich and efficient metaprogramming features of Lean 4. The random forest is trained on data extracted from mathlib -- Lean's mathematics library. We experiment with various options for producing training features and labels. The advice from a trained model is accessible to the user via the suggest_premises tactic which can be called in an editor while constructing a proof interactively.