# crush: Extensible Proof Automation for Lean

> Crush proves higher-order Lean goals to SMT solvers via mechanized defunctionalization, achieving 94% verification coverage and outperforming all baselines.

- **Source:** [arXiv](https://arxiv.org/abs/2610.40538)
- **Published:** 2026-10-31
- **Permalink:** https://picx.dev/p/Jvz9sY
- **Whiteboard:** https://picx.dev/p/Jvz9sY/image

## Summary

# Crush: Extensible Proof Automation for Lean

## Summary (Overview)

- **Crush** is an extensible SMT-backed proof automation framework for the Lean proof assistant that bridges the gap between Lean's higher-order, polymorphic logic and first-order SMT solvers.
- The framework employs **defunctionalization** to encode higher-order functions (including lambdas, partial applications, and function-valued arguments) into first-order SMT logic, with a **mechanized soundness proof** in Lean itself.
- Crush provides **extensible translation interfaces** (head-indexed and type-indexed rewrite rules) allowing users to customize how Lean types, functions, and operators are encoded to SMT without modifying the core translator.
- It supports **two proof reconstruction paths**: unsat core-guided search using native Lean tactics, and full replay of solver inference steps (Alethe format) via extensible rewrite rules.
- In evaluation across 754 verification conditions from four benchmark suites (Curated, Cashmere, Velvet, PLean), crush discharges **709 VCs (94.0%)** when trusting the solver and **693 (91.9%)** with kernel-checked proofs, outperforming all baselines including auto (82.5%), grind (85.0%), lean-smt, and Duper.

## Introduction and Theoretical Foundation

### Background and Motivation

The paper addresses the integration of automated theorem provers (ATPs) with proof assistants (PAs). While PAs like Lean, Rocq, Isabelle/HOL, and Agda provide rich type systems supporting higher-order and polymorphic constructs, ATPs like Z3, CVC5, and E-Prover offer powerful automation but support less expressive (typically first-order) logics.

The two main challenges in this integration are:

1. **Translation (ITP → ATP)**: Translating expressive proof obligations (with polymorphism, higher-order functions, user-defined abstractions) into the solver's first-order logic.
2. **Proof Reconstruction (ATP → ITP)**: Reconstructing kernel-checkable proofs from solver certificates (unsat cores or proof scripts).

### Limitations of Existing Approaches

The paper highlights key gaps in existing tools for Lean:

- **lean-auto**: Supports polymorphism but lacks higher-order function support, custom encodings, and proof reconstruction.
- **LeanHammer**: Supports higher-order functions but lacks extensible encodings and replay.
- **lean-smt**: Supports extensible encodings and replay but not higher-order functions.
- **grind** and **aesop**: Native Lean tactics with good proof production but limited to internal decision procedures.

**Table 1 (from paper)**: Qualitative comparison of goal translation and proof reconstruction.

| ITP | Tool | Poly. | HO | Ext. encoding | Core-guided | Replay |
|-----|------|-------|----|---------------|-------------|--------|
| Isabelle/HOL | smt | ✓ | ✓ | ✓ | × | ✓ |
| Rocq | SMTCoq | × | × | ✓ | × | ✓ |
| Rocq | CoqHammer | ✓ | ✓ | × | ✓ | × |
| Lean | lean-auto | ✓ | × | × | × | × |
| Lean | LeanHammer | ✓ | ✓ | × | ✓ | × |
| Lean | lean-smt | ✓ | × | ✓ | × | ✓ |
| Lean | **crush** | ✓ | ✓ | ✓ | ✓ | ✓ |

## Methodology

### 3. Extensible Lean-to-SMT Translation

Crush provides two mechanisms for translating Lean terms into SMT:

#### 3.1 Definition Unfolding
The `@[crush_unfold]` attribute exposes defining equations of functions to the SMT query. For example:

```lean
@[crush_unfold]
def clamp (x lo hi : Int) : Int :=
    if x < lo then lo
    else if hi < x then hi else x

theorem clamp_bounds (x lo hi : Int) (h : lo ≤ hi) :
    lo ≤ clamp x lo hi ∧ clamp x lo hi ≤ hi := by
  crush
```

#### 3.2 Head- and Type-Indexed Term Translation

Let $e^{\flat}$ denote the SMT term produced from a Lean expression $e$, and $\tau^{\flat}$ denote the SMT sort used to represent a Lean type $\tau$.

- **Head-indexed translation**: Rewrite rules matching the head symbol of an application. E.g., for the NAND function:
  $$(\text{Nand } x \; y)^{\flat} = \mathsf{bvnand}(x^{\flat}, y^{\flat})$$

- **Type-indexed translation**: Rewrites grouped by type, e.g., handling both `Bool.not` and `Bool.xor` under a `Bool` type pattern.

#### 3.3 Coordinating Sort and Term Translation

Users can define rewrite rules over type applications to encode custom Lean types. For example, `TotalMap κ ν` can be encoded as SMT Array sort, with `get` → `select` and `set` → `store`. Crush performs light-weight sort checking on emitted queries to catch incompatible sort/term translations.

### 4. Higher-Order Translation via Defunctionalization

#### 4.1 Defunctionalization

For a nondependent function type $\theta = \sigma_1 \rightarrow \dots \rightarrow \sigma_n \rightarrow \tau$ (where $\tau$ is not a function type), crush introduces:

1. An uninterpreted sort $\mathsf{Fn}_{\theta}$ for function values.
2. An application symbol with signature:
$$\mathsf{app}_{\theta}: \mathsf{Fn}_{\theta} \times \sigma_{1}^{\flat} \times \dots \times \sigma_{n}^{\flat} \to \tau^{\flat}$$

**Lambdas and captured variables**: For each lambda $\ell = \lambda x_1 \dots x_n.\; e$, a fresh uninterpreted symbol $\mathsf{clos}_{\ell}$ is introduced, with axiom:
$$\forall \bar{y}, \bar{x}. \quad \mathsf{app}_{\theta}(\mathsf{clos}_{\ell}(\bar{y}), \bar{x}) = e^{\flat}$$
where $\bar{y}$ are captured variables.

**Partial application**: η-expansion transforms partial applications into closures. **Function equality**: Extensionality axioms are emitted when comparing function values. **Guarded subtypes** (e.g., `Nat` within `Int`) are represented with guards like $x \geq 0$.

#### 4.2 Soundness of Defunctionalization

The paper formalizes higher-order (HO) and first-order (FO) languages with denotational semantics (Fig. 8), then proves:

**Theorem 1 (Soundness)**: For every finite collection $T$ of closed higher-order formulas, if $\mathcal{D}(T)$ is unsatisfiable, then $T$ is unsatisfiable.

Key definitions include:
- **Defunctionalization** $\mathcal{F}(e) = (e^{\flat}, C_e, E_e)$ where $C_e$ are closure equations and $E_e$ are extensionality axioms.
- **First-order encoding**: $\mathcal{D}(T) = \bigcup_{\varphi \in T} \left(C_{\varphi} \cup E_{\varphi} \cup \{\varphi^{\flat}\}\right)$

The proof uses a **canonical model extension** $M^{\star}$ interpreting Fn sorts as function spaces:
$$\llbracket \mathsf{Fn}_{\theta} \rrbracket_{M^{\star}} = \llbracket \theta \rrbracket_{M}$$

### 5. Proof Reconstruction

Crush supports two reconstruction approaches:

#### 5.1 Core-Guided Reconstruction
- Maps unsat core assertions back to Lean hypotheses
- Searches for proofs using native Lean tactics (e.g., `omega`, `grind`)
- Extensible via `@[crush_reconstruct]` theorem hints

#### 5.2 Extensible Solver Inference Replay
- Replays Alethe proof scripts from SMT solvers
- `register_crush_replay term`: maps SMT operators to Lean terms (type-checked by kernel)
- `register_crush_replay rule`: translates solver inference steps to Lean proofs

Example: handling `bv-not-idemp` rule using `BitVec.not_not` lemma: $\sim(\sim x) = x$

## Empirical Validation / Results

### 6. Evaluation Setup

- **754 VCs** across four suites: Curated (20), Cashmere (38), Velvet (504), PLean (192)
- **Baselines**: lean-auto (auto), Duper, lean-smt, Grind
- **Hardware**: Apple M1 Pro, 32 GB RAM
- **Solver**: CVC5 1.3.4
- **Limits**: 5s per solver call, 1M Lean heartbeats per tactic

### 6.1 Verification Coverage

| Method | VCs Discharged | Percentage |
|--------|---------------|------------|
| **crush (trusted)** | 709 | 94.0% |
| **crush (kernel-checked)** | 693 | 91.9% |
| grind | 641 | 85.0% |
| auto | 622 | 82.5% |
| lean-smt | 431 | 57.2% |
| Duper | 413 | 54.8% |

Crush achieves the highest overall coverage even with kernel-checked proofs required. Runtime curves show a tradeoff: grind is faster on many VCs but crush achieves higher overall coverage.

### 6.2 Pairwise Comparison

**Table 2 (from paper)**: Head-to-head comparison with crush using proof reconstruction.

| Benchmark | Baseline | crush only | Baseline only | Both |
|-----------|----------|------------|---------------|------|
| Curated (20) | auto | 2 | 0 | 17 |
| Curated | Duper | 8 | 1 | 11 |
| Curated | lean-smt | 7 | 0 | 12 |
| Curated | grind | 3 | 0 | 16 |
| Cashmere (38) | auto | 20 | 0 | 18 |
| Cashmere | Duper | 17 | 0 | 21 |
| Cashmere | lean-smt | 21 | 0 | 17 |
| Cashmere | grind | 19 | 0 | 19 |
| Velvet (504) | auto | 70 | 13 | 402 |
| Velvet | Duper | 184 | 3 | 288 |
| Velvet | lean-smt | 180 | 10 | 292 |
| Velvet | grind | 37 | 9 | 435 |
| PLean (192) | auto | 2 | 10 | 162 |
| PLean | Duper | 75 | 0 | 89 |
| PLean | lean-smt | 65 | 1 | 99 |
| PLean | grind | 2 | 0 | 162 |

Crush discharges more VCs in all pairs except against `auto` on PLean (2 vs. 10).

### 6.3 Proof Reconstruction Analysis

**Table 3 (from paper)**: Proof reconstruction failures among 503 VCs discharged by SMT.

| Method | Failure mode | VCs |
|--------|-------------|-----|
| Alethe replay alone | Certificate generation | 431 |
| | Term decoding | 1 |
| | Total | 432/503 |
| Combined | Certificate generation + core-guided failure | 11 |
| | Lean heartbeat limit | 2 |
| | Tactic failure during replay | 3 |
| | Total | 16/503 |

Key finding: **Adding core-guided reconstruction** enables crush to close many more VCs (693 vs. 241 with Alethe replay alone, vs. 431 for lean-smt). The main limitation is that CVC5 cannot generate Alethe proofs for all theories (particularly arrays).

**Table 4 (from paper)**: Implementation size of built-in Alethe replay extensions.

| Category | Handlers | Handler LoC | Lemma LoC | Total |
|----------|----------|-------------|-----------|-------|
| Assumption normalization | 2 | 16 | 34 | 50 |
| Logic and equality | 10 | 47 | 10 | 57 |
| Quantifiers | 1 | 3 | 22 | 25 |
| Arithmetic | 17 | 68 | 311 | 379 |
| Bitvectors | 13 | 72 | 337 | 409 |
| Strings | 12 | 50 | 83 | 133 |
| **Total** | **55** | **256** | **797** | **1,053** |

## Theoretical and Practical Implications

### Theoretical Contributions

1. **Mechanized soundness proof**: Unlike tools like CoqHammer that have informal soundness arguments with known approximation issues, crush formally proves the soundness of its defunctionalization pass in Lean itself, providing strong correctness guarantees.

2. **First-class treatment of higher-order functions**: The defunctionalization approach with explicit application symbols, closure axioms, and extensionality provides a principled bridge between higher-order and first-order logic.

3. **Extensible architecture**: The pattern-based translation and replay interfaces separate the core pipeline from user extensions, allowing customization without compromising the core's soundness.

### Practical Implications

1. **Improved verification coverage**: Crush discharges 94.0% of VCs (91.9% with proofs), significantly outperforming native tactics (grind: 85.0%) and existing SMT integrations (lean-smt: 57.2%, Duper: 54.8%).

2. **Kernel-level trust**: All reconstructed proofs are independently checked by the Lean kernel, maintaining the highest level of trustworthiness.

3. **Low implementation overhead for extensions**: The replay library required only 1,053 LoC for 55 handlers covering six theory categories, demonstrating the practicality of the extension interface.

4. **Flexible integration**: Crush works both as a standalone tactic and as a backend for third-party automation systems like Loom.

## Conclusion

### Main Takeaways

Crush successfully addresses the two main challenges of ATP-PA integration:
1. **Translation**: Supports higher-order, polymorphic Lean constructs via defunctionalization with a mechanized soundness proof.
2. **Proof reconstruction**: Combines unsat core-guided search with extensible Alethe proof replay for kernel-checked proofs.

The framework outperforms all baselines across diverse benchmark suites covering verification, distributed protocols, and general mathematics, achieving high coverage even when kernel-checked proofs are required.

### Future Work

The authors identify several directions for future research:

1. **Dependent function types**: Extending the supported fragment beyond nondependent higher-order constructs.
2. **Broader soundness formalization**: Extending beyond defunctionalization to the full Lean-to-SMT-LIB translation.
3. **Additional proof integrations**: Integrating tactics like Duper, supporting CPC certificates, and synthesizing non-emptiness proofs for choice expressions in solver certificates.
4. **Better SAT feedback**: Distinguishing true vs. spurious counter-examples when the solver reports SAT.

### Data Availability

The implementation, mechanized proofs, benchmark data, and reproduction scripts are publicly available at: https://github.com/AD1024/lean-crush/tree/tacas-ae

---

_Markdown view of https://picx.dev/p/Jvz9sY, served by PicX — AI-generated visual whiteboard summaries of research papers._