Elamur Research⌕
☰
home / papers / 2025 / Premise Selection for a Lean Hammer

Premise Selection for a Lean Hammer

Paper · 2025 · Thomas Zhu, Joshua Clune, Jeremy Avigad et al.

Summary

Lean users often have to name, by hand, the exact lemmas that justify each small proof step, drawn from libraries with hundreds of thousands of facts. Other proof assistants handle this with a hammer, but Lean has lacked a general-purpose one. The authors build LeanPremise, a neural premise selector trained with contrastive learning. Its training data comes from a hammer-aware extraction pipeline that produces (state, premise) pairs. At runtime it also indexes the user's own local lemmas and libraries it never saw in training. They combine it with Aesop (proof search), Lean-auto (translation from dependent type theory to higher-order logic), the Zipperposition prover, and Duper (proof reconstruction). The result is LeanHammer, the first end-to-end, domain-general hammer for Lean, callable as an ordinary tactic. On Mathlib, LeanHammer proves 21% more goals with LeanPremise than with existing premise selectors, and it transfers well to unseen projects in miniCTX-v2. This gives practitioners cheap, low-latency automation that needs no large LLM, and it links neural retrieval with symbolic proving.

Key points

  • Pipeline: Aesop runs first. It tries its own rules, then applies retrieved premises directly. Remaining subgoals go to Lean-auto, which translates them into TH0 for Zipperposition. Duper then rebuilds a Lean proof from only the premises the prover actually used.
  • Model sizes: LeanPremise comes in small (23M), medium (33M) and large (82M) versions, compared against ReProver (218M). Proof rate grows with selector size.
  • Retrieval settings: a sweep fixed 16 premises for Lean-auto and 32 premises as Aesop application rules.
  • Speed and scope: most successful calls finish in under 1 second. Solved theorems mostly have 1–2-line human proofs and use at most about 8 ground-truth premises, so the tool is best at closing small gaps.
  • Error analysis (Mathlib-test, auto setting, large model): 26.7% of goals failed translation and 50.4% were translated but not proved. 21.3% were solved, versus 33.1% when the ground-truth premises were supplied.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang and Sean Welleck. 2025. Premise Selection for a Lean Hammer. arXiv:2506.07477.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2506.07477 · arXiv 2506.07477

@misc{zhu2025premise,
  title = {{Premise Selection for a Lean Hammer}},
  author = {Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang and Sean Welleck},
  year = {2025},
  doi = {10.48550/arxiv.2506.07477},
  eprint = {2506.07477},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2506.07477}
}

References

58 references, 31 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver.…
  2. Lasse Blaauwbroek, Mirek Olsák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Online representation learning of formal math concepts. In Forty-Proof rate (%) aesop auto aesop+auto full cumul 29.8 29.3 28.6 29.4 22.6 20.0 20.0 21.2 30.2 28.5 28.4 29.0 34.…
  3. OpenReview.net, 2024. URL https://openreview.net/forum?id=A7CtiozznN. ↗
  4. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109–128, 2013. doi: 10.1007/S10817-013-9278-5. — [doi:10.1007/s10817-013-9278-5](https://doi.org/10.1007/s10817-013-9278-5) find
  5. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C Paulson, and Josef Urban. Hammering towards qed. Journal of Formalized Reasoning, 9(1):101–148, 2016.
  6. Mario Carneiro, Chad E. Brown, and Josef Urban. Automated Theorem Proving for Metamath. In Adam Naumowicz and René Thiemann (eds.), Interactive Theorem Proving (ITP), pp. 9:1–9:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi: 10.4230/LIPIcs.ITP.2023.9. — [doi:10.4230/lipics.itp.2023.9](https://doi.org/10.4230/lipics.itp.2023.9) find
  7. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025.
  8. Joshua Clune, Yicheng Qian, Alexander Bentkamp, and Jeremy Avigad. Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. In Yves Bertot, Temur Kutsia, and Michael Norrish (eds.), Interactive Theorem Proving (ITP), volume 309, pp. 10:1– 10:20, Dagstuhl, Germany, 2024. Schlo…
  9. Lukasz Czajka and C. Kaliszyk. Hammer for Coq: Automation for dependent type theory. Journal of Automated Reasoning, 61:423 – 453, 2018. URL https://api.semanticscholar.org/CorpusID:11060917. ↗
  10. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof (eds.), Tools and Algorithms for the Construction and Analysis of Systems, pp. 337– 340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. doi: 10.1007/978-3-540-78800-3_24. find
  11. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe (eds.), Conference On Automated Deduction (CADE), pp. 625–635. Springer, 2021. doi: 10.1007/978-3-030-79876-5_37.
  12. Kefan Dong and Tengyu Ma. Beyond limited data: Self-play llm theorem provers with iterative conjecturing and proving. arXiv preprint arXiv:2502.00212, 2025.
  13. Matthijs Douze, Alexandr Guzhva, Chengqi Deng, Jeff Johnson, Gergely Szilvasy, Pierre-Emmanuel Mazaré, Maria Lomeli, Lucas Hosseini, and Hervé Jégou. The faiss library. arXiv preprint arXiv:2401.08281, 2024.
  14. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Satish Chandra, Kelly Blincoe, and Paolo Tonella (eds.), Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of…
  15. ACM, 2023. doi: 10.1145/3611643.3616243. URL https://doi.org/10.1145/3611643.3616243. — [doi:10.1145/3611643.3616243](https://doi.org/10.1145/3611643.3616243) ↗
  16. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Proceedings of the 2015 Conference on Certified Programs and Proofs, New York, NY, USA, January 2015. ACM. find
  17. Jiewen Hu, Thomas Zhu, and Sean Welleck. miniCTX: Neural theorem proving with (long-)contexts. In The Thirteenth International Conference on Learning Representations, 2025. URL https://openreview.net/forum?id=KIgaAqEFHW. ↗
  18. Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, pp. 378–392, 2021. find
  19. Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Adva…
  20. Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothée Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In International Conference on Learning Representations (ICLR). OpenReview.net,…
  21. Cezary Kaliszyk and Josef Urban. Hol(y)hammer: Online ATP service for HOL light. Mathematics in Computer Science, 9(1):5–22, 2015a. doi: 10.1007/s11786-014-0182-0.
  22. Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. Journal of Automated Reasoning, 55(3): 245–256, 2015b. doi: 10.1007/s10817-015-9330-8.
  23. Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, and Emily First. Cobblestone: Iterative automation for formal verification. CoRR, abs/2410.19940, 2024. doi: 10.48550/ARXIV.2410.19940. URL https://doi.org/10.48550/arXiv.2410.19940. — [doi:10.48550/arxiv.2410.19940](https://doi.org/10.48550/arxiv.2410.19940) ↗
  24. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith (eds.), Computer Aided Verification (CAV), pp. 1–35, Berlin, Heidelberg, 2013. Springer. find
  25. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. Mash: machine learning for sledgehammer. In Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings 4, pp. 35–50. find
  26. Guillaume Lample, Timothée Lacroix, Marie-Anne Lachaux, Aurélien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. In Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (eds.), Advances in Neural In…
  27. Lean Community. Completion of the liquid tensor experiment. blog post, 2022. URL https://leanprover-community.github.io/blog/posts/lte-final/. ↗
  28. Jannis Limperg and Asta Halkjær From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 253–266, 2023. find
  29. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025a.
  30. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613, 2025b.
  31. Minghai Lu, Benjamin Delaware, and Tianyi Zhang. Proof automation with large language models. In Vladimir Filkov, Baishakhi Ray, and Minghui Zhou (eds.), Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE 2024, Sacramento, CA, USA, October 27 - November… find
  32. ACM, 2024. doi: 10.1145/3691620.3695521. URL https://doi.org/10.1145/3691620.3695521. — [doi:10.1145/3691620.3695521](https://doi.org/10.1145/3691620.3695521) ↗
  33. Jia Meng and Lawrence C Paulson. Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic, 7(1):41–57, 2009. find
  34. Jia Meng, Claire Quigley, and Lawrence C. Paulson. Automation for interactive proof: First prototype. Information and Computation, 204(10):1575–1596, 2006. doi: https://doi.org/10.1016/j.ic.2005.05.010. — [doi:10.1016/j.ic.2005.05.010](https://doi.org/10.1016/j.ic.2005.05.010) ↗
  35. Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. In The Twelfth International Conference on Learning Representation…
  36. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002. doi: 10.1007/3-540-45949-9. — [doi:10.1007/3-540-45949-9](https://doi.org/10.1007/3-540-45949-9) find
  37. Aaron van den Oord, Yazhe Li, and Oriol Vinyals. Representation learning with contrastive predictive coding. arXiv preprint arXiv:1807.03748, 2018.
  38. Lawrence Charles Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In IWIL@LPAR, 2012. URL https://api.semanticscholar.org/CorpusID:598752. ↗
  39. Bartosz Piotrowski, Ramon Fernández Mir, and Edward Ayers. Machine-learned premise selection for lean. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp. 175–186. Springer, 2023. find
  40. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023.
  41. OpenReview.net, 2023. URL https://openreview.net/forum?id=-P7G-8dmSh4. ↗
  42. Yicheng Qian, Joshua Clune, Clark Barrett, and Jeremy Avigad. Lean-auto: An interface between lean 4 and automated theorem provers. In Lecture Notes in Computer Science, Lecture notes in computer science, pp. 175–196. Springer Nature Switzerland, Cham, 2025. find
  43. Nils Reimers and Iryna Gurevych. Sentence-bert: Sentence embeddings using siamese bert-networks. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing. Association for Computational Linguistics, 11 2019. URL https://arxiv.org/abs/1908.10084. ↗
  44. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In Pascal Fontaine (ed.), Conference on Automated Deduction (CADE), pp. 495–507. Springer, 2019.
  45. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Lean copilot: Large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534, 2024.
  46. Terence Tao. Formalizing the proof of pfr in lean4 using blueprint: a short tour. blog post, 2023. URL https://terrytao.wordpress.com/2023/11/18/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour/. ↗
  47. Yicheng Tao, Haotian Liu, Shanwen Wang, and Hongteng Xu. Assisting mathematical formalization with a learning-based premise retriever. arXiv preprint arXiv:2501.13959, 2025. — [arXiv:2501.13959](https://arxiv.org/abs/2501.13959) find
  48. The Mathlib Community. The lean mathematical library. In Jasmin Blanchette and Catalin Hritcu (eds.), Certified Programs and Proofs (CPP), pp. 367–381. ACM, 2020. doi: 10.1145/3372885.3373824.
  49. Floris van Doorn, Patrick Massot, and Oliver Nash. Formalising the h-principle and sphere eversion. In Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (eds.), Certified Programs and Proofs (CPP), pp. 121–134. ACM, 2023. doi: 10.1145/3573105.3575688. — [doi:10.1145/3573105.3575688](https://doi.org/10.1145/3573105.3575688) find
  50. Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin, and Sophie Tourret. Making higher-order superposition work. Journal of Automated Reasoning, 66: 541–564, 2022. doi: 10.1007/s10817-021-09613-z. — [doi:10.1007/s10817-021-09613-z](https://doi.org/10.1007/s10817-021-09613-z) find
  51. Haiming Wang, Huajian Xin, Chuanyang Zheng, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, and Xiaodan Liang. Lego-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vi…
  52. OpenReview.net, 2024. URL https://openreview.net/forum?id=3f5PALef5B. ↗
  53. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025.
  54. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024.
  55. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. CoRR, abs/2405.14333, 2024a. doi: 10.48550/ARXIV.2405.14333. URL https://doi.org/10.48550/arXiv.2405.14… ↗
  56. Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-… — DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  57. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Neural Information Processing Systems (NeurIPS), 2023.
  58. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. CoRR, abs/2305.16366, 2023. doi: 10.48550/ARXIV.2305.16366. URL https://doi.org/10.48550/arXiv.2305.16366. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhu-2025-premise-selection-lean-hammer/