← All repos

lean-smt

Tactics for discharging Lean goals into SMT solvers.

GitHub
lean4smt
Browse cluster: Lean4 Formal Verification & Cryptography →
197commits
16contributors
1languages

Tech stack & purpose

Lean-SMT provides Lean tactics that translate proof goals into SMT solver queries, send them to the cvc5 solver, and replay the returned proofs back in Lean. The project is built for Lean 4 and currently supports theories of uninterpreted functions, linear integer and real arithmetic with quantifiers, and experimental support for bitvectors. It integrates with the lean-auto library for monomorphization of dependent type theory into first-order logic, and uses Mathlib for real arithmetic reasoning. The project is maintained by ufmg-smite and is actively developed, though currently in beta phase.

Community & reference links

Languages

Lean
100.0%

Contributors