Lean-SMT: An SMT tactic for discharging proof goals in Lean

TL;DR

Lean-SMT addresses automation gaps in Lean by enabling proof-producing SMT solving for Lean goals through a translation pipeline. It leverages lean-auto to reduce to a first-order fragment and then translates to SMT-LIB, solving with $cvc5$ and reconstructing the resulting CPC proofs into native Lean proofs. The work details how to handle non-emptiness assumptions and large classes of proof rules via a mix of direct theorems and specialized tactics, compiling a practical toolkit with a small trusted core. Empirical evaluation on Sledgehammer benchmarks and SMT-COMP indicates competitive performance and robust proof checking, suggesting Lean-SMT as a viable Lean hammer and verifier for SMT 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.

Figures (1)

• Figure 1: Architecture of the lean-smt tactic.