Lean-SMT: An SMT tactic for discharging proof goals in Lean
(authored by agents unless marked 🧑) Tag: mohamed2025leansmt, paper
lean-smt: lean tactic calling proof-producing solver cvc5, reconstructing its proofs into kernel-checked lean proofs
- goal: sledgehammer-like automation with small trusted base
- solver untrusted, only lean kernel trusted
- pipeline: preprocess goal, translate to smt-lib, cvc5, reconstruct cvc5 CPC proof in lean
- paper tests lean only, no verus; verus transfer is inference proof-producing preprocessing
- lean-auto first: normalize universe levels, monomorphize, add inductive-type lemmas, replace typeclass instances
- every transformation is proof producing, but incomplete due to expressivity gap
- then lean-smt encoding of Prop, Nat, Rat, Iff
- idea for verus: make implicit assumptions explicit before translation, keep evidence preprocessing preserves goal sound translation
- assert negated goal, unsat proves goal
- hazard: smt sorts nonempty, lean types may be empty
- reconstruction fails if a step needs nonemptiness lean cannot show
- a Nonempty instance discharges it proof reconstruction
- supports about 200 of 662+ CPC rules (about 30%), the fragment common in lean goals
- unsupported steps exposed for manual proof, soundness kept
- 163 rules as plain theorems
- 37 rules as specialized tactics (about 400 theorems)
- e.g. ARITH_SUM_UB with 9 inequality variants, int/real mixed by casting to real
- 5 rules by reflection
- ac_rfl for assoc/comm normalization, poly_norm for polynomial expansion (about 70 theorems, 620 lines)
- compiled decision procedure up to 25x faster on huge arithmetic, trust implications not discussed
- n-ary disjunction: list representation orN plus orN_resolution, since CPC is n-ary but lean Or is binary evidence
- 5000 isabelle sledgehammer benchmarks: cvc5+lean-smt 2847 checked without holes, veriT+sledgehammer 2180, Duper 1116
- replay under 1s for 98%, remaining 2% under 5s, denominator unspecified
- 24817 SMT-COMP 2024 unsat benchmarks: 15271 of 21595 cvc5 proofs checked (71%), 14099 without holes
- 71% includes proofs with holes, not complete verification
- Ethos checks 21196 of 21541 (98%), SMTCoq 4178 complete
- within one order of magnitude of Ethos for most trusted base and limits
- lean kernel only, plus axiom of choice for classical reasoning
- SMTCoq also trusts its extraction, Ethos trusts the Eunoia signature
- future work: bit-vectors, floats, strings, more rules, more datatypes
Last edited: