“Lean-smt: An SMT Tactic for Discharging Proof Goals in Lean” by Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett. In Proceedings of the 37^th International Conference on Computer Aided Verification (CAV '25), (Ruzica Piskac and Zvonimir Rakamaric, eds.), July 2025, pp. 197-212. Zagreb, Croatia.
Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A key aspect of Sledgehammer is the use of proof-producing SMT solvers to prove a translated proof goal and the reconstruction of the resulting proof into valid justifications for the original goal. We present lean-smt, a tactic providing this functionality in Lean. We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs. We evaluate the tactic on established benchmarks used to evaluate Sledgehammer's SMT integration, with promising results. We also evaluate lean-smt as a standalone proof checker for proofs of SMT-LIB problems. We show that lean-smt offers a smaller trusted core without sacrificing too much performance.
BibTeX entry:
@inproceedings{MMK+25,
author = {Abdalrhman Mohamed and Tomaz Mascarenhas and Harun Khan and
Haniel Barbosa and Andrew Reynolds and Yicheng Qian and Cesare
Tinelli and Clark Barrett},
editor = {Ruzica Piskac and Zvonimir Rakamari{\'c}},
title = {Lean-smt: An {SMT} Tactic for Discharging Proof Goals in Lean},
booktitle = {Proceedings of the {\it 37^{th}} International Conference
on Computer Aided Verification (CAV '25)},
series = {Lecture Notes in Computer Science},
volume = {15931},
pages = {197--212},
publisher = {Springer},
month = jul,
year = {2025},
doi = {10.1007/978-3-031-98682-6_11},
note = {Zagreb, Croatia},
url = {https://doi.org/10.1007/978-3-031-98682-6_11}
}
(This webpage was created with bibtex2web.)