{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:17:20Z","timestamp":1767928640438,"version":"3.49.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Proof automation is crucial to large-scale formal mathematics and software\/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose\u00a0proof automation in ITPs such as Coq and Isabelle, leveraging the power of ATPs. An important component of a hammer is the translation algorithm from the ITP\u2019s logical system to the ATP\u2019s logical system. In this paper, we propose a novel translation algorithm for ITPs based on dependent type theory. The algorithm is implemented in Lean 4\u00a0under the name Lean-auto. When combined with ATPs, Lean-auto provides general-purpose, ATP-based proof automation in Lean 4 for the first time. Soundness of the main translation procedure is guaranteed, and experimental results suggest that our algorithm is sufficiently complete to automate the proof of\u00a0many problems that arise in practical uses of Lean 4. We also find that Lean-auto solves more problems than existing tools on Lean 4\u2019s math library Mathlib4.<\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_10","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:14:43Z","timestamp":1753154083000},"page":"175-196","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Lean-Auto: An Interface Between Lean 4 and\u00a0Automated Theorem Provers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-0194-9572","authenticated-orcid":false,"given":"Yicheng","family":"Qian","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4047-6196","authenticated-orcid":false,"given":"Joshua","family":"Clune","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1275-315X","authenticated-orcid":false,"given":"Jeremy","family":"Avigad","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"10_CR1","unstructured":"Avigad, J., de\u00a0Moura, L., Kong, S., Ullrich, S.: Theorem Proving in Lean4 (2025). https:\/\/leanprover.github.io\/theorem_proving_in_lean4"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"10_CR3","unstructured":"Barendregt, H.P.: Lambda calculi with types, pp. 117\u2013309. Oxford University Press, Inc., USA (1993). https:\/\/dl.acm.org\/doi\/10.5555\/162552.162561"},{"key":"10_CR4","unstructured":"Barras, B., et al.: The Coq proof assistant: reference manual, version 6.1 (1997). https:\/\/api.semanticscholar.org\/CorpusID:54117279"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Bhayat, A., Suda, M.: A higher-order Vampire (short paper). In: Benzm\u00fcller, C., Heule, M.J., Schmidt, R.A. (eds.) Automated Reasoning, pp. 75\u201385. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_5","DOI":"10.1007\/978-3-031-63498-7_5"},{"key":"10_CR6","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9, 101\u2013148 (2016). https:\/\/api.semanticscholar.org\/CorpusID:218028818"},{"key":"10_CR7","unstructured":"B\u00f6hme, S.: Proving Theorems of Higher-Order Logic with SMT Solvers. Ph.D. thesis, Technical University Munich (2012). https:\/\/nbn-resolving.org\/urn:nbn:de:bvb:91-diss-20120511-1084525-1-4"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-03359-9_6","volume-title":"Theorem Proving in Higher Order Logics","author":"A Bove","year":"2009","unstructured":"Bove, A., Dybjer, P., Norell, U.: A brief overview of Agda \u2013 a functional language with dependent types. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 73\u201378. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_6"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Carneiro, M., Brown, C.E., Urban, J.: Automated theorem proving for Metamath. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0268, pp. 9:1\u20139:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.9","DOI":"10.4230\/LIPIcs.ITP.2023.9"},{"key":"10_CR10","unstructured":"Clune, J., Qian, Y., Bentkamp, A., Avigad, J.: Duper: a proof-producing superposition theorem prover for dependent type theory. In: International Conference on Interactive Theorem Proving (2024). https:\/\/api.semanticscholar.org\/CorpusID:272330518"},{"issue":"2","key":"10_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2), 95\u2013120 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3","journal-title":"Inf. Comput."},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50\u201366. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_47"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. 61, 423 \u2013 453 (2018). https:\/\/api.semanticscholar.org\/CorpusID:11060917","DOI":"10.1007\/s10817-018-9458-4"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hall, C.V., Hammond, K., Jones, S.L.P., Wadler, P.: Type classes in Haskell. In: TOPL (1994). https:\/\/api.semanticscholar.org\/CorpusID:9227770","DOI":"10.1007\/3-540-57880-3_16"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/3-540-61511-3_97","volume-title":"Automated Deduction \u2014 Cade-13","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: Optimizing proof search in model elimination. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 313\u2013327. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61511-3_97"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Harrison, J., Urban, J., Wiedijk, F.: History of interactive theorem proving. In: Computational Logic (2014). https:\/\/api.semanticscholar.org\/CorpusID:30345151","DOI":"10.1016\/B978-0-444-51624-4.50004-6"},{"key":"10_CR17","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical Reports, pp. 56\u201368 (2003). https:\/\/api.semanticscholar.org\/CorpusID:11201048"},{"issue":"1","key":"10_CR18","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2014). https:\/\/doi.org\/10.1007\/s11786-014-0182-0","journal-title":"Math. Comput. Sci."},{"issue":"3","key":"10_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: MizAR 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9330-8","journal-title":"J. Autom. Reason."},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Limperg, J., From, A.H.: Aesop: white-box best-first proof search for Lean. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, pp. 253\u2013266. Association for Computing Machinery, New York (2023). https:\/\/doi.org\/10.1145\/3573105.3575671","DOI":"10.1145\/3573105.3575671"},{"key":"10_CR22","unstructured":"Miku\u0142a, M., et al.: Magnushammer: a transformer-based approach to premise selection. arXiv (2024). https:\/\/arxiv.org\/abs\/2303.04488"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Ullrich, S.: The Lean 4 theorem prover and programming language. In: CADE (2021). https:\/\/api.semanticscholar.org\/CorpusID:235800962","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"10_CR25","unstructured":"Paulson, L.C.: A generic tableau prover and its integration with Isabelle. J. Univers. Comput. Sci. 5, 73\u201387 (1999). https:\/\/api.semanticscholar.org\/CorpusID:2551237"},{"key":"10_CR26","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL@LPAR (2012). https:\/\/api.semanticscholar.org\/CorpusID:598752"},{"key":"10_CR27","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. arXiv abs\/2009.03393 (2020). https:\/\/api.semanticscholar.org\/CorpusID:221535103"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Qian, Y., Clune, J., Barrett, C., Avigad, J.: Lean-auto: an interface between lean 4 and automated theorem provers (2025). https:\/\/arxiv.org\/abs\/2505.14929","DOI":"10.1007\/978-3-031-98682-6_10"},{"issue":"2","key":"10_CR29","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1080\/10586458.2021.1926016","volume":"31","author":"P Scholze","year":"2022","unstructured":"Scholze, P.: Liquid tensor experiment. Exp. Math. 31(2), 349\u2013354 (2022). https:\/\/doi.org\/10.1080\/10586458.2021.1926016","journal-title":"Exp. Math."},{"key":"10_CR30","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15, 111\u2013126 (2002). https:\/\/api.semanticscholar.org\/CorpusID:884116"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-319-08970-6_32","volume-title":"Interactive Theorem Proving","author":"M Sozeau","year":"2014","unstructured":"Sozeau, M., Tabareau, N.: Universe polymorphism in Coq. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 499\u2013514. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_32"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"The Mathlib Community: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367\u2013381. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"10_CR33","doi-asserted-by":"publisher","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making higher-order superposition work. J. Autom. Reason. 66(4), 541\u2013564 (2022). https:\/\/doi.org\/10.1007\/s10817-021-09613-z","DOI":"10.1007\/s10817-021-09613-z"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Blanchette, J.C., Schulz, S.: Extending a high-performance prover to higher-order logic. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (2023). https:\/\/api.semanticscholar.org\/CorpusID:249226027","DOI":"10.1007\/978-3-031-30820-8_10"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: International Conference on Theorem Proving in Higher Order Logics (2008). https:\/\/api.semanticscholar.org\/CorpusID:13752195","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"10_CR36","unstructured":"Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. arXiv abs\/1905.09381 (2019). https:\/\/api.semanticscholar.org\/CorpusID:162184110"},{"key":"10_CR37","unstructured":"Yang, K., et al.: Leandojo: Theorem proving with retrieval-augmented language models. arXiv abs\/2306.15626 (2023). https:\/\/api.semanticscholar.org\/CorpusID:259262077"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:38:46Z","timestamp":1759999126000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Clark Barrett is an Amazon Scholar.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}