![[2506.07477] Premise Selection for a Lean Hammer](https://arxiv.org/static/browse/0.3.4/images/arxiv-logo-fb.png){kind=logo}
[2506.07477] Premise Selection for a Lean Hammer
Summary
The paper presents LeanPremise, a neural premise selection system that enhances LeanHammer, a tool for automated reasoning in proof assistants, improving goal-solving efficiency by 21%.
Why It Matters
This research addresses the integration of neural methods into practical verification workflows, making formal verification more accessible. By improving premise selection, it enhances the performance of proof assistants, which are crucial for ensuring the correctness of software and systems.
Key Takeaways
- LeanPremise is designed for effective premise selection in Lean proof assistant workflows.
- It adapts to user-specific contexts, recommending relevant premises beyond its training data.
- The system improves goal-solving efficiency by 21% compared to existing selectors.
- LeanHammer integrates premise selection, translation, and proof reconstruction into a unified tool.
- This work bridges neural retrieval and symbolic reasoning, enhancing formal verification.
Computer Science > Machine Learning arXiv:2506.07477 (cs) [Submitted on 9 Jun 2025 (v1), last revised 25 Feb 2026 (this version, v2)] Title:Premise Selection for a Lean Hammer Authors:Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck View a PDF of the paper titled Premise Selection for a Lean Hammer, by Thomas Zhu and Joshua Clune and Jeremy Avigad and Albert Qiaochu Jiang and Sean Welleck View PDF HTML (experimental) Abstract: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...
