An SMT hammer for Lean 4. Write by crush to solve goals involving arithmetic,
equalities, bitvectors, datatypes, and higher-order functions.
- Higher-order translation: supports function arguments, partial applications, and lambdas through defunctionalization or cvc5's native higher-order mode.
- Checked proofs: reconstructs Lean proofs from unsat cores or replays cvc5's Alethe certificates. Solver trust is explicit and auditable.
- Extensible translation: custom lowerings and replay rules use the same interfaces as the built-in theories.
See the user manual for the full guide, configuration reference, and extension APIs.
Use the Lean version in lean-toolchain and install a solver on
PATH: Z3 ≥ 4.15.4 (the default), cvc5 ≥ 1.3.4, or Bitwuzla. cvc5 additionally
supports Alethe replay and native higher-order solving; Bitwuzla supports a
restricted quantifier-free fragment and does not provide proof certificates or
unsat cores. The package has no third-party Lean dependencies.
Add to your lakefile.lean, then run lake update:
require crush from git "https://github.com/AD1024/lean-crush" @ "main"import Crush
example (x y : Int) (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
crush
example (f : Int → Int) (a b : Int) (h : a = b) : f a = f b := by
crush
example (g : (Int → Int) → Int) (h : ∀ f, g f = f 1) :
g (fun x => x + 1) = 2 := by
crushBy default, an SMT discharge trusts the solver using the Crush.crushSorry
axiom. Its proof retains dependencies from the asserted facts and from encoding
evidence, including Nonempty and LawfulBEq proofs, for #print axioms to
report. To require a Lean proof, use the reconstruction policy below.
Bare crush introduces binders and uses all local hypotheses. Select facts or
supply extra lemmas with:
crush [h, myLemma] -- only the listed hypotheses and lemmas
crush [*, myLemma] -- all local hypotheses, plus a lemma
crush u[myFn] -- unfold a definition using its equationsDefinition equations may also be added automatically. Mark a definition with
@[crush_unfold], or enable unfolding for an existing one:
attribute [local crush_unfold] List.length
example (xs : List Int) : xs.length = 0 ↔ xs = [] := by
crushPolymorphic lemmas are specialized to relevant types, and a bounded instantiation pass supplies ground facts before solving. See Using the Tactic for fact selection, unfolding, induction examples, and premise search.
set_option crush.trust "reconstruct" in
theorem checked (x y : Int) (hxy : x = y) (hy : y = 3) : x = 3 := by
crush
#print axioms checkedThis policy fails if reconstruction cannot produce a checked proof. The default
reconstruction portfolio can use cvc5's Alethe certificate and an unsat-core
fallback; Z3 uses core reconstruction. Some goals close with a checked proof
before SMT even under the default trust policy. Use #print axioms to inspect
dependencies.
Checked reconstruction rejects dependencies on sorryAx or Crush.crushSorry,
including definitions mentioned in the goal or hypotheses used by a proof.
When an admission blocks reconstruction, the error or reconstructOrTrust
fallback warning identifies the forbidden axiom and the definition that depends
on it. A rejected candidate does not prevent a later checked proof from succeeding.
Common settings include:
set_option crush.backend "cvc5"
set_option crush.trace.script trueSee Configuration for trust policies, replay modes, timeouts, and debugging options.
A lowering maps a Lean expression to an SMT term:
open Crush
def addThree (x : Int) : Int := x + 3
register_lowering term <<
(addThree (term x)) => (smt| (+ $x 3))
>>
example (x : Int) : addThree x = x + 3 := by crush(term x) recursively translates the captured expression; a bare x captures
its Lean.Expr. The RHS can also be a metaprogram. The same syntax supports
register_lowering result-type and register_lowering sort.
Custom lowerings are part of the trusted translation boundary: their authors
must preserve the Lean operation's semantics.
Use register_crush_replay for custom Alethe term decoding and inference rules,
and @[crush_reconstruct] for core reconstruction lemmas. See
Extending lean-crush
and Test/AletheExtension.lean for complete examples.
- Induction is explicit. Use Lean's
inductiontactic, then letcrushclose the cases using the induction hypotheses. - Translation is incomplete. Unsupported operations may remain uninterpreted;
supply lemmas, unfold definitions, or add a lowering. Native SMT bitvectors
require concrete widths. Built-in sorts cannot depend on variables bound
inside translated quantifiers or lambdas, including type variables and
propositions occurring in function domains. Function values with proof domains
(
p → βforp : Prop) are also refused, even when closed; fully applied functions may still erase proof arguments when the existing guards permit it. - Unsupported premises can be omitted. Solver queries skip hypotheses that
fail translation, undoing their translation state and reporting them under
trace.crush. Failure to translate the negated goal remains an error. Script-only mode (crush.backend "none") warns about each omitted premise. - Empty-carrier guards can slow quantified solving. Lean types may be empty,
while SMT sorts are always inhabited. The required validity guards can increase
solver search substantially. For an opaque type
T, justified[Nonempty T]evidence or an existing local valuex : Tlets translation omit its guard. Expose nonemptiness only when it follows from the problem's assumptions. - Solving can exceed reconstruction. A solver may prove a goal whose certificate or core cannot yet be reconstructed in Lean.
- Models describe the encoding. A satisfiable SMT model is not necessarily a counterexample to the original Lean proposition.
See Troubleshooting for unsupported cases and diagnostic options.
lake build # library
lake build Test.Smoke # quick solver integration check
lake build Test # full dependency-free test suiteRunnable examples live in Test/, with verification conditions in
Test/CaseStudies/ and optional Mathlib integration in
MathlibTest/. Read the
optimization guide before changing search bounds or
reconstruction heuristics.
For recorded results, see BENCHMARKS.md and the manual's
coverage and reconstruction figures.
To run the experiments:
bash run-experiments.shThe first run provisions and builds the benchmark projects and can take hours.
Use --suites curated for the smallest suite; see the
benchmark script guide for prerequisites, resuming runs,
plotting, and individual harnesses.
@misc{he2026crushextensibleproofautomation,
title={crush: Extensible Proof Automation for Lean},
author={Mike He and Dexin Zhang and Aarti Gupta},
year={2026},
eprint={2610.40538},
archivePrefix={arXiv},
primaryClass={cs.LO},
url={https://arxiv.org/abs/2610.40538},
}lean-auto informed the design and supplies test material. Verification case studies draw on Loom, Velvet, Cashmere, Cedar, and Strata. Veil informs the planned model minimization.