Lean-SMT: An SMT tactic for discharging proof goals in Lean
Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark Barrett
cs.LO
May 21, 2025 · v1
TL;DR
Lean-SMT is a Lean tactic that discharges goals via proof-producing SMT solvers and reconstructs SMT proofs into native Lean proofs.
Abstract
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.
Problem
Lean lacks important automation features present in more mature proof assistants, particularly SMT solver integration analogous to Isabelle/HOL's Sledgehammer tactic for automatically discharging proof goals.
Approach
Lean-SMT converts Lean goals into SMT problems, sends them to a proof-producing SMT solver (cvc5), and reconstructs the resulting SMT proofs into native Lean proofs. The reconstruction handles the core SMT-LIB logics including quantifier-free linear arithmetic, bitvectors, and uninterpreted functions. The architecture ensures correctness by producing Lean-kernel-checked proof terms rather than trusting the external solver.
Results
Evaluation on established Sledgehammer benchmarks shows promising results. As a standalone proof checker for SMT-LIB problems, Lean-SMT offers a smaller trusted core than existing SMT proof checkers without sacrificing too much performance.
