grind: An SMT-Inspired Tactic for Lean 4

Kim Morrison, Leonardo de Moura
Lean FRO | AWS and Lean FRO

IJCAR 2026, Lisbon | July 2026

What Is `grind`?

A virtual whiteboard, inspired by modern SMT solvers.

Writes facts on the board. Merges equivalent terms.
Cooperating engines: congruence closure, E-matching, constraint propagation, guided case analysis.
Satellite theory solvers: cutsat (linear integer arithmetic), commutative rings (Gröbner), linarith, AC.
Native to dependent type theory. No translation to FOL.
Produces ordinary Lean proof terms. Kernel-checkable.
5,000+ grind uses in Mathlib.

Lean Goal

→

Preprocessing

→

Internalization

→

E-graph

↔

cutsat

↔

rings

↔

linarith

↔

orders

↔

`grind` — Theory Combination

example [CommRing α] [NoNatZeroDivisors α]
    (a b c : α) (f : α → Nat)
    : a + b + c = 3 →
      a^2 + b^2 + c^2 = 5 →
      a^3 + b^3 + c^3 = 7 →
      f (a^4 + b^4) + f (9 - c^4) ≠ 1 := byα:Type u_1inst✝¹:CommRing αinst✝:NoNatZeroDivisors αa:αb:αc:αf:α → Nat⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → f (a ^ 4 + b ^ 4) + f (9 - c ^ 4) ≠ 1
  grindAll goals completed! 🐙

Three solvers meet at the E-graph:

Ring solver derives a^4 + b^4 = 9 - c^4.
Congruence closure lifts it to f (a^4 + b^4) = f (9 - c^4).
Linear integer arithmetic closes 2 * f (9 - c^4) ≠ 1.

The Nelson-Oppen playbook. Inside dependent type theory. No SMT translation layer.

`grind` — Typeclass-Parameterized Theory Solvers

Satellite solvers activate automatically when the type classes are present.

Ring — CommRing, CommSemiring, Field, IsCharP, NoNatZeroDivisors.
linarith — module over the integers. Preorders, partial, linear orders.
AC — any associative-commutative operator.

-- BitVec 8 is a CommRing of characteristic 256.
-- No bitvector-specific theory needed.
example (x : BitVec 8) : (x - 16) * (x + 16) = x^2 := byx:BitVec 8⊢ (x - 16) * (x + 16) = x ^ 2
  grindAll goals completed! 🐙

-- Bitwise Or is AC and idempotent
example (x y w z: Nat)
    : x ||| z = w ||| x → z ||| y ||| x ||| x = x ||| y ||| w := byx:Naty:Natw:Natz:Nat⊢ x ||| z = w ||| x → z ||| y ||| x ||| x = x ||| y ||| w
  grindAll goals completed! 🐙

`grind` — Annotations and E-Matching

Library authors annotate theorems; grind instantiates them by E-matching — pattern matching modulo the E-graph.

[grind =] — use the LHS as the E-matching pattern.
[grind →] — forward reasoning: patterns from hypotheses.
[grind ←] — backward reasoning: patterns from the conclusion.
grind_pattern — custom multi-patterns.
Constraint system on patterns: guard, check, is_value, is_strict_value.

@[grind =] theorem fg {x} : f (g x) = x := byx:Nat⊢ f (g x) = x
  unfold f gx:Nat⊢ 2 * x / 2 = x; omegaAll goals completed! 🐙

example {a b c} : f a = b → a = g c → b = c := bya:Natb:Natc:Nat⊢ f a = b → a = g c → b = c
  grindAll goals completed! 🐙

`grind` — Interactive Mode

grind => exposes a domain-specific language for stepping through the solver's execution. You can mix grind steps with ordinary tactics.

example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := byx:R⊢ (cos x + sin x) ^ 2 = 2 * cos x * sin x + 1
  grind =>
    instantiate only [trig_identity]grindx:Rh✝:¬(cos x + sin x) ^ 2 = 2 * cos x * sin x + 1⊢ False
    ringAll goals completed! 🐙

Both humans and AI can control grind.

example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := byx:R⊢ (cos x + sin x) ^ 2 = 2 * cos x * sin x + 1
  grind?All goals completed! 🐙Try these:
  [apply] grind only [trig_identity]
  [apply] grind =>
    instantiate only [trig_identity]
    ring

Extensible: Users can add new grind tactics and solvers.

`grind` — Diagnostics

example (as bs cs : Array α) (v : α) (i : Nat)
        (h₁ : i < as.size)
        (h₂ : bs = as.set i v)
        (h₅ : j < bs.size)
        (h₆ : j < as.size)
        : bs[j] = as[j] := byα:Type u_1j:Natas:Array αbs:Array αcs:Array αv:αi:Nath₁:i < as.sizeh₂:bs = as.set i v h₁h₅:j < bs.sizeh₆:j < as.size⊢ bs[j] = as[j]
  grindAll goals completed! 🐙`grind` failed
grind.1α:Type u_1j:Natas bs cs:Array αv:αi:Nath₁:i < as.sizeh₂:bs = as.set i v h₁h₅:j < bs.sizeh₆:j < as.sizeh:¬bs[j] = as[j]h_1:i = j⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] i + 1 ≤ as.size
[prop] bs = as.set i v ⋯
[prop] j + 1 ≤ bs.size
[prop] j + 1 ≤ as.size
[prop] ¬bs[j] = as[j]
[prop] (as.set i v ⋯).size = as.size
[prop] (as.set i v ⋯)[j] = if i = j then v else as[j]
[prop] i = j
[eqc] True propositions
[prop] j + 1 ≤ as.size
[prop] j + 1 ≤ bs.size
[prop] i + 1 ≤ as.size
[prop] j < as.size
[prop] j < bs.size
[prop] i < as.size
[prop] i = j
[prop] j < (as.set i v ⋯).size
[eqc] False propositions
[prop] bs[j] = as[j]
[eqc] Equivalence classes
[eqc] {j, i}
[eqc] {bs, as.set i v ⋯}
[eqc] {v, bs[j], (as.set i v ⋯)[j]}
[eqc] {if i = j then v else as[j]}
[eqc] {as.size, bs.size, (as.set i v ⋯).size}
[eqc] {j + 1, i + 1}
[eqc] {as.size = 0, bs.size = 0}
[eqc] others
[eqc] {↑j, ↑i}
[eqc] {↑as.size, ↑bs.size, ↑(as.set i v ⋯).size}
[cases] Case analyses
[cases] [1/2]: if i = j then v else as[j]
[cases] source: E-matching `Array.getElem_set`
[ematch] E-matching patterns
[thm] Array.eq_empty_of_size_eq_zero: [@Array.size #2 #1]
[thm] Array.size_set: [@Array.size #4 (@Array.set _ #3 #2 #1 #0)]
[thm] Array.getElem_set: [@getElem (Array #6) `[Nat] _ _ _ (@Array.set _ #5 #4 #2 #3) #1 #0]
[cutsat] Assignment satisfying linear constraints
[assign] j := 0
[assign] i := 0
[assign] as.size := 1
[assign] bs.size := 1
[assign] (as.set i v ⋯).size := 1
[ring] Ring `Int`
[basis] Basis
[_] ↑i + -1 * ↑j = 0
[_] ↑as.size + -1 * ↑bs.size = 0
[_] ↑bs.size + -1 * ↑(as.set i v ⋯).size = 0

[grind] Diagnostics
[thm] E-Matching instances
[thm] Array.getElem_set ↦ 1
[thm] Array.size_set ↦ 1

Conclusion

grind is a new extensible tactic based on SMT techniques.

Grind reference manual

New features and performance improvements are in development.

We expect AI systems will use grind => interactive mode.

Maintaining formal proofs is as hard as writing them in the first place.

lean-lang.org

Thank You

Leo de Moura
lean-lang.org
leanprover.zulipchat.com

grind reference manual

IJCAR 2026, Lisbon | July 2026

grind: An SMT-Inspired Tactic for Lean 4

What Is grind?

grind — Theory Combination

grind — Typeclass-Parameterized Theory Solvers

grind — Annotations and E-Matching

grind — Interactive Mode

grind — Diagnostics