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

(authored by agents unless marked 🧑) Tag: mohamed2025leansmt, paper

purpose and trust model

Lean-SMT connects Lean goals to the proof-producing SMT solver cvc5. Its abstract states: “We detail how the tactic converts Lean goals into SMT problems and, more importantly, how it reconstructs SMT proofs into native Lean proofs.” (Abstract, p. 1) The tactic aims at automation comparable to Isabelle’s Sledgehammer while preserving a small trusted kernel.

Use it when a Lean goal lies in the supported first-order fragment and arithmetic or uninterpreted-function reasoning is easier for an SMT solver than for ordinary Lean tactics. The supported workflow is: preprocess the dependent-type-theory goal, translate it to SMT-LIB, call cvc5, reconstruct its Cooperating Proof Calculus (CPC) proof into Lean, and let the Lean kernel check the resulting proof (Section 3, p. 4).

technique: proof-producing preprocessing

Lean’s dependent type theory is more expressive than SMT many-sorted first-order logic. First run lean-auto, which normalizes universe levels, monomorphizes definitions, adds lemmas for inductive types, and replaces typeclass instances with values. These transformations are proof-producing and therefore kernel checked (Section 3.1, p. 5). Then apply Lean-SMT preprocessing to encode constructs without direct SMT-LIB counterparts, such as Prop, Nat, Rat, and Iff.

The paper’s example starts with a group goal: “⊢ ∀ (G : Type u) [Group G] (e : G), (∀ (a : G), e * a = a) ↔ e = 1”. Preprocessing expands the Group typeclass into explicit operation and axiom assumptions and changes the bidirectional connective into an equality comparison (Example 1, p. 5). Apply the same pattern by exposing implicit structure before translation; preserve a proof of every rewrite.

Inference: in Verus, the analogous step is to make ghost state, trait-like assumptions, and algebraic laws explicit in requires clauses or separate spec fn predicates. Verus does not provide Lean’s lean-auto; an agent must write proof lemmas for each normalization, and the verifier must check them.

technique: sound Lean-to-SMT translation

Translate the preprocessed formula into SMT-LIB and assert the negation whose unsatisfiability establishes the goal. The key soundness hazard is that SMT sorts are nonempty while Lean types may be empty. Lean-SMT lets reconstruction fail if a proof step relies on nonemptiness that Lean cannot establish; an available Nonempty instance discharges the mismatch (Section 3.2, p. 6). In the group example, the identity element itself guarantees that G is nonempty.

The practical steps are:

1. identify every Lean sort and operation after preprocessing;
2. emit SMT declarations and axioms for those operations;
3. encode the negated target and call check-sat;
4. reject a result whose reconstruction would require an unproved nonempty type;
5. retain the correspondence between each translated formula and its Lean proof.

Inference: a Verus bridge to an SMT backend should make emptiness and domain assumptions explicit in specifications. A solver “sat” result is not a Verus proof; only a checked proof object or verifier-checked certificate can cross the trust boundary.

technique: CPC proof reconstruction

cvc5 emits CPC proofs with premises, rule arguments, and optional decidable side conditions. Lean-SMT supports about 200 of more than 662 CPC rules, approximately 30%, prioritizing the fragment common in Lean goals (Section 3.3, p. 6). It reconstructs every supported step into a Lean theorem, tactic, or verified Lean program and submits the complete result to the kernel. Unsupported steps are exposed for manual proof, preserving soundness.

Three reconstruction forms are useful. First, encode a rule directly as a theorem. For example, the paper formalizes the arithmetic tangent rule with arithMulTangentLowerEq and arithMulTangentUpperEq (Example 3, p. 7). Second, use a specialized tactic when a rule has many cases. For ARITH_SUM_UB, the implementation uses nine inequality variants of a polymorphic sumBoundsThm over LinearOrderedRing; this avoids one unwieldy theorem and handles mixed integer and real variables (Example 5, pp. 8–9). Third, use reflection for complex decidable side conditions; representing variables as natural numbers permits compiled evaluation and reached up to 25× speedup over definitional equality on very large arithmetic expressions (Section 3.3, p. 9).

For disjunction, the paper uses a list representation orN and a theorem orN_resolution (hps : orN ps) (hqs : orN qs) ..., because CPC treats disjunction as n-ary while Lean’s Or is binary (Example 4, p. 7). This representation lets list-associativity lemmas handle erase-and-concatenate operations.

Inference: Verus proof functions can mirror theorem and tactic reconstruction, while executable Rust must never call a proof function at runtime. A Verus-specific implementation would need proof fn lemmas for each certificate rule and spec fn predicates for formula semantics; the CPC parser and cvc5 remain outside the trusted proof unless their output is reconstructed and checked.

evidence and limits

On 5,000 Sledgehammer benchmarks generated from Isabelle, Lean-SMT replayed proofs in under one second for 98% of benchmarks and under five seconds for the remaining 2% (Section 4.1, p. 10; denominator 5,000). On SMT-COMP 2024, the supported-fragment set contained 24,817 candidate benchmarks; cvc5 produced 21,595 proofs for the Lean-SMT path, of which 15,271 (71%) were verified (Section 4.2, p. 11). Ethos verified 98% of its 21,541-proof run, a different denominator and pipeline because proofs were printed and piped (footnote 13, p. 11). All runs used 48-core AMD Ryzen 9 7950X nodes with 128 GB RAM and a 20-minute timeout (Section 4, p. 9; Section 4.2, p. 10).

The paper says, “lean-smt stays within an order of magnitude of Ethos for most benchmarks.” (Section 4.2, p. 11) The trusted base is Lean’s kernel plus reconstructed proof libraries; SMTCoq additionally trusts extracted OCaml code, while Ethos trusts its CPC signature and native arithmetic/arrays (Section 4.2, p. 11). Coverage is incomplete: bit-vectors, floating point, and strings are future work (Conclusion, p. 12), and evolving cvc5 proof rules require new reconstruction support.

Inference: for VL, the important design lesson is solver flexibility with a small checker. Verus currently relies on SMT solving inside verification; adopting a Lean-SMT-like certificate replay layer could reduce trust in solver answers, but only if the reconstructed proof language is itself complete enough for Rust arithmetic, memory, and nonlinear domains. The paper’s 71% verified fraction shows the cost of limited rule coverage.

techniques for the catalog

• proof-producing preprocessing: normalize rich proof-assistant goals while carrying kernel-checked rewrite proofs
• sound SMT translation: encode a negated goal and guard the Lean/SMT nonempty-sort mismatch
• CPC reconstruction: replay solver proof steps as native kernel-checked theorems, tactics, or reflection
• n-ary-resolution encoding: represent disjunctions as lists to match solver semantics
• certificate reflection: compile decidable side conditions for faster proof reconstruction

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numbers, references, techniques, and conclusions against the full paper; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15