{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:52Z","timestamp":1771888192522,"version":"3.50.1"},"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>Lean is an increasingly popular proof assistant based on dependent\u00a0type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic\u00a0in Isabelle\/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to\u00a0prove a translated proof goal and the reconstruction of the resulting proof into\u00a0valid justifications for the original goal. We present <jats:sc>lean-smt<\/jats:sc>, a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and,\u00a0more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer\u2019s SMT integration, with promising results. We also evaluate <jats:sc>lean-smt<\/jats:sc> as a standalone proof checker for proofs of SMT-LIB problems. We show that <jats:sc>lean-smt<\/jats:sc> offers a smaller trusted core without sacrificing too much performance.<\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_11","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:14:52Z","timestamp":1753154092000},"page":"197-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["lean-smt: An SMT Tactic for Discharging Proof Goals in Lean"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1414-7073","authenticated-orcid":false,"given":"Abdalrhman","family":"Mohamed","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2747-8349","authenticated-orcid":false,"given":"Tomaz","family":"Mascarenhas","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3379-5631","authenticated-orcid":false,"given":"Harun","family":"Khan","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0194-9572","authenticated-orcid":false,"given":"Yicheng","family":"Qian","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"11_CR1","unstructured":"Avigad, J., de\u00a0Moura, L., Kong, S., Ullrich, S.: Theorem proving in Lean 4. https:\/\/leanprover.github.io\/theorem_proving_in_lean4\/"},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Baanen, A.: Formalizing Fundamental Algebraic Number Theory. Phd-thesis - research and graduation internal, Vrije Universiteit Amsterdam (2024). https:\/\/doi.org\/10.5463\/thesis.541","DOI":"10.5463\/thesis.541"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A Versatile and Industrial-Strength SMT Solver (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) International Joint Conference on Automated Reasoning (IJCAR). Lecture Notes in Computer Science, vol. 13385, pp. 15\u201335. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"11_CR5","doi-asserted-by":"publisher","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification (CAV), pp. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"11_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. In: Bj\u00f8rner, N.S., Sofronie-Stokkermans, V. (eds.) Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31\u2013August 5, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06803, pp. 116\u2013130. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_11","DOI":"10.1007\/978-3-642-22438-6_11"},{"issue":"1","key":"11_CR9","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reasoning"},{"key":"11_CR10","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364 (2011)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-Solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"11_CR12","doi-asserted-by":"publisher","unstructured":"Castelvecchi, D.: Mathematicians welcome computer-assisted proof in \u201cgrand unification\u201d theory. Nature 595 (2021). https:\/\/doi.org\/10.1038\/d41586-021-01627-2","DOI":"10.1038\/d41586-021-01627-2"},{"key":"11_CR13","doi-asserted-by":"publisher","unstructured":"Clune, J., Qian, Y., Bentkamp, A., Avigad, J.: Duper: a proof-producing superposition theorem prover for dependent type theory. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0309, pp. 10:1\u201310:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.10, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2024.10","DOI":"10.4230\/LIPIcs.ITP.2024.10"},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"mathlib Community, T.: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 367\u2013381. CPP 2020. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Desharnais, M., Vukmirovic, P., Blanchette, J., Wenzel, M.: Seventeen provers under the hammer. In: Andronick, J., de\u00a0Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7\u201310, 2022, Haifa, Israel. LIPIcs, vol.\u00a0237, pp. 8:1\u20138:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2022.8","DOI":"10.4230\/LIPICS.ITP.2022.8"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-319-63390-9_7","volume-title":"Computer Aided Verification","author":"B Ekici","year":"2017","unstructured":"Ekici, B., Mebsout, A., Tinelli, C., Keller, C., Katz, G., Reynolds, A., Barrett, C.: SMTCoq: a plug-in for integrating SMT solvers into Coq. In: Majumdar, R., Kun\u010dak, V. (eds.) Computer Aided Verification, pp. 126\u2013133. Springer International Publishing, Cham (2017)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A mathematical Introduction to Logic, 2 edn. Academic Press (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore, December 15\u201317, 2007. Revised and Invited Papers. Lecture Notes in Computer Science, vol.\u00a05081, p.\u00a0333. Springer (2007). https:\/\/doi.org\/10.1007\/978-3-540-87827-8_28","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"11_CR19","unstructured":"Hales, T., et al.: A formal proof of the kepler conjecture (2015)"},{"key":"11_CR20","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers in proc (2003). https:\/\/api.semanticscholar.org\/CorpusID:11201048"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., et al.: Mizar 60 for mizar 50. In: Naumowicz, A., Thiemann, R. (eds.) Interactive Theorem Proving (ITP). LIPIcs, vol.\u00a0268, pp. 19:1\u201319:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.19","DOI":"10.4230\/LIPICS.ITP.2023.19"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Kaliszyk, C., Urban, J.: Hol(y)hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015). https:\/\/doi.org\/10.1007\/s11786-014-0182-0","DOI":"10.1007\/s11786-014-0182-0"},{"key":"11_CR23","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010). https:\/\/doi.org\/10.1145\/1743546.1743574","DOI":"10.1145\/1743546.1743574"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Lachnitt, H., et al.: Isarare: automatic verification of SMT rewrites in isabelle\/hol. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part I. Lecture Notes in Computer Science, vol. 14570, pp. 311\u2013330. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_17","DOI":"10.1007\/978-3-031-57246-3_17"},{"key":"11_CR25","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. pp. 253\u2013266. CPP 2023. Association for Computing Machinery, New York (2023). https:\/\/doi.org\/10.1145\/3573105.3575671","DOI":"10.1145\/3573105.3575671"},{"key":"11_CR26","doi-asserted-by":"publisher","unstructured":"Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Inf. Comput. 204(10), 1575\u20131596 (2006). https:\/\/doi.org\/10.1016\/j.ic.2005.05.010","DOI":"10.1016\/j.ic.2005.05.010"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Mohamed, A., et al.: Lean-SMT: an SMT tactic for discharging proof goals in Lean (2025). https:\/\/arxiv.org\/abs\/2505.15796","DOI":"10.1007\/978-3-031-98682-6_11"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"11_CR29","unstructured":"Nelson, L., Geffen, J.V., Torlak, E., Wang, X.: Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In: 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4\u20136, 2020, pp. 41\u201361. USENIX Association (2020). https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/nelson"},{"key":"11_CR30","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., et al.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: Griggio, A., Rungta, N. (eds.) Formal Methods In Computer-Aided Design (FMCAD), pp. 65\u201374. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_12","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_12"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Piotrowski, B., Mir, R.F., Ayers, E.: Machine-learned premise selection for Lean (2023). https:\/\/arxiv.org\/abs\/2304.00994","DOI":"10.1007\/978-3-031-43513-3_10"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"P\u00eerlea, G., Gladshtein, V., Kinsbruner, E., Zhao, Q., Sergey, I.: Veil: a framework for automated and interactive verification of transition systems. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 21\u201325, 2025, Proceedings. Lecture Notes in Computer Science, Springer (2025)","DOI":"10.1007\/978-3-031-98682-6_2"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Qian, Y., Clune, J., Barrett, C., Avigad, J.: Lean-auto: an interface between lean 4 and automated theorem provers. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 21\u201325, 2025, Proceedings. Lecture Notes in Computer Science. Springer (2025), to appear","DOI":"10.1007\/978-3-031-98682-6_10"},{"key":"11_CR35","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). CoRR abs\/2107.02354 (2021). https:\/\/arxiv.org\/abs\/2107.02354"},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12699, pp. 450\u2013467. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26","DOI":"10.1007\/978-3-030-79876-5_26"},{"key":"11_CR37","doi-asserted-by":"publisher","unstructured":"Tao, T.: Machine assisted proof. AMS Notices 72(1), 86\u201395 (2025). https:\/\/doi.org\/10.1090\/noti3041","DOI":"10.1090\/noti3041"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:39:07Z","timestamp":1759999147000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_11","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 Interest"}},{"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"}}]}}