LeanHammer automates tedious proof steps in Lean. Given a goal, it selects relevant premises, translates them to higher-order logic, calls external automated theorem provers, and reconstructs verified proofs.
LeanHammer incorporates a new hammer-aware premise selector along with Lean-auto for translation, Duper for proof reconstruction, and Aesop for proof search into a new hammer architecture.
LeanHammer shows an ability to close goals in Mathlib and generalize to projects it was not trained on, such as those in miniCTX-v2, and dynamically adapts to user-specific contexts, including new premises from local projects.
For installation instructions, see the GitHub repository.
Call the hammer tactic on proof goals:
import LeanHammer
example (n : ℕ) : n + 0 = n := by
hammer
LeanHammer is callable as a tactic in Lean. The premise selector runs on an external server with low computational cost and latency.
For more details, see the GitHub repository and the paper.
@article{zhu2025leanhammer,
title={Premise Selection for a Lean Hammer},
author={Zhu, Thomas and Clune, Joshua and Avigad, Jeremy and Jiang, Albert Q. and Welleck, Sean},
journal={arXiv preprint arXiv:2506.07477},
year={2025}
}