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

TL;DR

Lean-SMT introduces an automation tactic in Lean that leverages SMT solvers to discharge proof goals, reconstructs proofs into Lean, and offers a lightweight, effective proof checking method.

Contribution

It presents a novel tactic for Lean that integrates SMT solving and proof reconstruction, filling a gap in Lean's automation capabilities.

Findings

Promising results on established benchmarks

Effective proof reconstruction into Lean

Smaller trusted core with competitive performance

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.