# Premise Selection for a Lean Hammer

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 56 references that are in the map.
- First posted on arXiv 9 Jun 2025.

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

- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Representation Learning with Contrastive Predictive Coding](https://mlsanity.com/paper/1807.03748/) (2018)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search](https://mlsanity.com/paper/2408.08152/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [Baldur: Whole-Proof Generation and Repair with Large Language Models](https://mlsanity.com/paper/2303.04910/) (2023)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving](https://mlsanity.com/paper/2305.16366/) (2023)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Proof Automation with Large Language Models](https://mlsanity.com/paper/2409.14274/) (2024)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [Machine-Learned Premise Selection for Lean](https://mlsanity.com/paper/2304.00994/) (2023)
- [HOL(y)Hammer: Online ATP Service for HOL Light](https://mlsanity.com/paper/1309.4962/) (2013)
- [Premise Selection and External Provers for HOL4](https://mlsanity.com/paper/1509.03534/) (2015)
- [Formalising the h-principle and sphere eversion](https://mlsanity.com/paper/2210.07746/) (2022)
- [Lean-auto: An Interface between Lean 4 and Automated Theorem Provers](https://mlsanity.com/paper/2505.14929/) (2025)

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

- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [Process-Verified Reinforcement Learning for Theorem Proving via Lean](https://mlsanity.com/paper/2606.20068/) (2026)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [When Agda met Vampire](https://mlsanity.com/paper/2602.18844/) (2026)
- [RePro: Proof-Verified Benchmark Rewriting for Reliable Evaluation of LLM Mathematical Problem Solving](https://mlsanity.com/paper/2609.00062/) (2026)

## Abstract (arXiv)

Neural methods are transforming automated reasoning for proof assistants, yet integrating these advances into practical verification workflows remains challenging. A hammer is a tool that integrates premise selection, translation to external automatic theorem provers, and proof reconstruction into one overarching tool to automate tedious reasoning steps. We present LeanPremise, a novel neural premise selection system, and we combine it with existing translation and proof reconstruction components to create LeanHammer, the first end-to-end domain general hammer for the Lean proof assistant. Unlike existing Lean premise selectors, LeanPremise is specifically trained for use with a hammer in dependent type theory. It also dynamically adapts to user-specific contexts, enabling it to effectively recommend premises from libraries outside LeanPremise's training data as well as lemmas defined by the user locally. With comprehensive evaluations, we show that LeanPremise enables LeanHammer to solve 21% more goals than existing premise selectors and generalizes well to diverse domains. Our work helps bridge the gap between neural retrieval and symbolic reasoning, making formal verification more accessible to researchers and practitioners.