Crush boosts proof automation for Lean with SMT solver support
crush: Extensible Proof Automation for Lean
Logic in Computer ScienceProgramming Languages
Summary
Proving mathematical statements in Lean is complicated because it uses advanced programming ideas that don’t fit neatly into simpler logic systems used by automated tools. The authors introduce crush, a framework that helps translate Lean’s complex proofs into a simpler form that external solvers can handle. It then carefully rebuilds proofs checked by Lean’s core to ensure trustworthiness. This approach can be extended by users and works better than previous tools at solving and verifying proof tasks.
What this means in practice
- •For formal verification engineers: Accelerate the verification of software and hardware properties by automating more proof obligations in Lean with reliable solver-backed tactics.
- •For proof assistant tool developers: Incorporate extensible SMT proof automation into new or existing Lean automation systems without rewriting core translation logic.
Authors
Mike He, Dexin Zhang, Aarti Gupta
Abstract
Lean's rich expressiveness supports higher-order functions, inductive datatypes, and user-defined abstractions, making it challenging to translate proof obligations into first-order Satisfiability Modulo Theory (SMT) queries and reconstruct kernel checked proofs. We present crush, an extensible SMT-backed proof automation framework for Lean. To bridge the gap between Lean's higher-order constructs and the solver's first-order logic, crush uses defunctionalization to encode function values and their applications. We formalize this translation for a supported higher-order fragment and prove its soundness. Moreover, crush provides metaprogramming interfaces for extending both Lean-to-SMT translation and the reconstruction of Lean proofs from solver certificates without modifying the translation pipeline. We implement crush as both a tactic and a backend for other third-party automation systems. We show that across four such use cases that target verification and general proof automation, crush discharges more obligations than the competing backends and reconstructs more kernel-checked proofs than the baselines.