Automated Lean Proofs for Every Type (www.galois.com)

This summer an intern at Galois built a Lean tactic that automates a large class of proofs by translating Lean types into SMT-friendly encodings and invoking a bitvector SMT decision procedure. Working on the Jolt zkVM frontend, they automatically translated ZMod → Nat → BitVectors and called the SMT bitvector solver (bv_decide / bit-blasting) to discharge lookup-table proofs. On 10 sampled Jolt tables the tactic solved all queries in under three minutes (while a finite-field SMT approach timed out on all but one), and it replaced roughly 6,800 lines of hand-written Lean proofs—saving an estimated 320 person-hours. The work highlights a crucial gap between ITPs (Lean) and SMT tools: types and encodings matter. SMT solvers have highly specialized decision procedures (integers, bitvectors, finite fields), but Lean’s rich types (Nat, Int, ZMod, UInt16, Fin, etc.) don’t map uniquely to those theories. The tactic combines AST traversal with type-specific range lemmas and selective case-splitting to handle variable dependencies that naive range reasoning or full case analysis would fail on (or make intractable). While the implemented translations are type-specific today, the approach suggests a practical hybrid: user-supplied type lemmas plus solver calls (or user-specified procedures) to handle dependencies. The result is a compelling step toward a general type-translation framework that would let users pick optimal SMT encodings and bring much more automation—and scalability—to real-world verification in Lean.