grind: An SMT-Inspired Tactic for Lean 4 (Short Paper — System Description)

grind: An SMT-Inspired Tactic for Lean 4 (Short Paper — System Description)

Kim MorrisonLeonardo de Moura

Kim Morrison (Lean FRO, kim@lean-fro.org) and Leonardo de Moura (Lean FRO and Amazon Web Services, leo@lean-fro.org, leomoura@amazon.com)

Table of Contents

  1. 1. Abstract
  2. 2. Introduction
  3. 3. grind by Example
  4. 4. Typeclass-Parametrized Solvers
  5. 5. Interactive Mode and Diagnostics
  6. 6. Related Work
  7. 7. Evaluation and Conclusion

1. Abstract🔗

We describe grind, an SMT-inspired proof automation tactic for Lean 4. Unlike hammer-style tools that translate proof obligations into external logics and invoke external ATP and SMT solvers, grind works natively in the Calculus of Inductive Constructions, producing kernel-checkable proof terms without any soundness compromises. At its core, grind combines congruence closure for dependent type theory with E-matching and a suite of satellite solvers for linear integer arithmetic, linear arithmetic over ordered modules, polynomial equations over commutative (semi)rings, and associative-commutative operators. Each satellite solver is parameterized by Lean's typeclasses, enabling it to operate over any type that implements the appropriate algebraic interface---not just hardcoded numeric types. Users can extend grind with new theory solvers through a plugin API, control theorem instantiation through instantiation constraints on E-matching patterns, and inspect the internal state through an interactive DSL. An annotation system, including automatic pattern selection, enables libraries to declare how their theorems should be used by grind. The tactic is distributed as part of Lean and is used extensively in Lean's Mathlib  (Community, 2020)The Mathlib Community, 2020. “The Lean Mathematical Library”. In Proc. CPP 2020. and CSLib  (Barrettet al, 2026)Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, and Sorrachai Yingchareonthawornchai, 2026. “CSLib: The Lean Computer Science Library”. arXiv:2602.04846 libraries.

2. Introduction🔗

Proof assistants based on dependent type theory---Coq  (Team, 2024)The Coq Development Team, 2024. “The Coq Proof Assistant”. In https://coq.inria.fr/. and Lean 4  (de Moura and Ullrich, 2021)Leonardo de Moura and Sebastian Ullrich, 2021. “The Lean 4 Theorem Prover and Programming Language”. In Proc. CADE-28, LNAI 12699.---provide strong guarantees: every accepted proof is checked by a small trusted kernel. The price is that constructing proofs often requires substantial manual effort.

Two families of automation dominate current practice. Rewriting-based tactics such as simp apply oriented equations exhaustively. Hammer-style tools translate goals into first-order or higher-order logic, invoke external provers, and reconstruct proofs internally. Sledgehammer  (Paulson and Blanchette, 2010)Lawrence C. Paulson and Jasmin Christian Blanchette, 2010. “Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers”. In Proc. IWIL 2010. pioneered this approach for Isabelle/HOL; CoqHammer  (Czajka and Kaliszyk, 2018)Łukasz Czajka and Cezary Kaliszyk (2018). “Hammer for Coq: Automation for Dependent Type Theory”. Journal of Automated Reasoning.61 pp. 423–453. adapted it for Coq; lean-auto  (Qianet al, 2025)Yicheng Qian, Joshua Clune, Clark Barrett, and Jeremy Avigad, 2025. “Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers”. In Computer Aided Verification. and LeanHammer  (Zhuet al, 2025)Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck, 2025. “Premise Selection for a Lean Hammer”. arXiv:2506.07477 bring it to Lean 4. Translation introduces a gap: not every feature of dependent type theory has a counterpart in the target logic, and reconstruction can fail even when the external prover succeeds.

grind takes a different approach. Inspired by the architecture of SMT solvers  (Barbosaet al, 2022)Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar, 2022. “cvc5: A Versatile and Industrial-Strength SMT Solver”. In Proc. TACAS 2022, LNCS 13243.  (de Moura and Bjørner, 2008)Leonardo de Moura and Nikolaj Bjørner, 2008. “Z3: An Efficient SMT Solver”. In Proc. TACAS 2008, LNCS 4963., it combines congruence closure, E-matching, and theory solvers into a single tactic operating directly on Lean expressions in the Calculus of Inductive Constructions. There is no translation step and no external tool: every proof term is checked by Lean's kernel. The congruence closure procedure handles the full Calculus of Inductive Constructions, extending earlier work  (Selsam and de Moura, 2016)Daniel Selsam and Leonardo de Moura, 2016. “Congruence Closure in Intensional Type Theory”. In Proc. IJCAR 2016, LNAI 9706..

Each satellite solver in grind is parameterized by Lean's typeclass mechanism. The linear arithmetic solver operates over any type equipped with a module structure over a semiring, and becomes incrementally more powerful over a ring or field. This design enables grind to handle the rich algebraic hierarchy found in mathematical libraries, without hardcoding specific types.

grind is open source (source code), distributed as part of Lean 4 with no external dependencies, and has been available since Lean 4.22 (August 2025). We recommend the reader consult the reference manual. The implementation comprises approximately 40,000 lines of Lean.

2.1. Contributions🔗

This paper describes grind with a focus on the following contributions.

  1. Native operation in the CIC. grind combines congruence closure, E-matching, and theory solvers in a single framework that operates directly on Lean expressions---including dependent types, dependent pattern matching, universe polymorphism, and proof irrelevance---producing kernel-checkable proof terms without translation to an external logic.

  2. Typeclass-parametrized solvers. Each satellite solver is parameterized by Lean typeclasses, activating automatically for any type with the required algebraic structure. This contrasts with traditional SMT solvers that hardcode specific types.

  3. Annotation and instantiation control. An annotation system with automatic pattern selection lets library authors declare how their theorems should be used by grind, and a constraint language on E-matching patterns restricts when theorems are instantiated (Section 2).

  4. Extensibility. All built-in solvers are implemented through the same plugin API available to users, who can register new theory solvers and constraint propagators without leaving Lean.

  5. Proof stability and diagnostics. grind? outputs self-contained invocations listing the theorems actually used, an interactive mode (grind =>) exposes the solver's execution step by step, and comprehensive failure diagnostics report equivalence classes, satellite solver states, and resource limits reached.

3. grind by Example🔗

All examples here can be explored interactively at https://live.lean-lang.org/.

3.1. Congruence closure🔗

At the core of grind is a congruence closure algorithm for dependent type theory  (Selsam and de Moura, 2016)Daniel Selsam and Leonardo de Moura, 2016. “Congruence Closure in Intensional Type Theory”. In Proc. IJCAR 2016, LNAI 9706.. It maintains equivalence classes over the terms. When two terms are known to be equal, congruence closure automatically deduces equalities between larger expressions built from them.

example (f : Nat → Nat) (h : a = b) : f (f b) = f (f a) := a:Natb:Natf:Nat → Nath:a = b⊢ f (f b) = f (f a) All goals completed! 🐙

Here grind notices the a = b hypothesis, applies congruence to obtain f a = f b, and then concludes f (f a) = f (f b). A contradiction is detected when the equivalence classes containing True and False are merged. Before adding terms to the E-graph, grind normalizes them: \beta-reduction, canonicalization of instances and implicit arguments, and hash-consing so that structural equality reduces to pointer equality.

3.2. E-matching and annotations🔗

While the Lean simp tactic uses theorems as rewriting rules, grind instantiates theorems using E-matching. Each theorem annotated for grind carries one or more patterns. Whenever the E-graph contains terms that match a pattern modulo known equalities, grind instantiates the theorem and asserts the result as a new fact.

open Lean Grind in def f' (x : Nat) := x - 1 open Lean Grind in def g' (x : Nat) := x + 1 @[grind =] theorem fg : f' (g' x) = x := x:Nat⊢ f' (g' x) = x All goals completed! 🐙 example : f' a = b → a = g' c → b = c := a:Natb:Natc:Nat⊢ f' a = b → a = g' c → b = c All goals completed! 🐙

The attribute [grind =] selects the left-hand side of the equation, f' (g' x), as the E-matching pattern. Although the goal does not contain a literal instance of f' (g' x), the hypothesis a = g' c allows grind to match f' a by substituting a with g' c modulo the known equality.

Library authors typically do not want to specify patterns manually for every theorem. grind provides a family of annotations that capture commonly used idioms. For equational theorems, [grind =] selects the left-hand side as the pattern, [grind _=_] selects both sides, and the bare [grind] attribute invokes an algorithm that traverses the conclusion and hypotheses left to right, collecting the minimal set of indexable subexpressions---those with a constant at the head---that cover all universally quantified variables. For implications, [grind →] extracts patterns from the hypotheses (forward reasoning) and [grind ←] from the conclusion (backward reasoning).

As an example of forward reasoning, consider annotating transitivity and symmetry lemmas for a relation R:

open Lean Grind in def R : Nat → Nat → Prop := (· % 7 = · % 7) @[grind →] theorem Rtrans : R x y → R y z → R x z := x:Naty:Natz:Nat⊢ R x y → R y z → R x z All goals completed! 🐙 @[grind →] theorem Rsymm : R x y → R y x := x:Naty:Nat⊢ R x y → R y x All goals completed! 🐙 example : R a b → R c b → R d c → R a d := a:Natb:Natc:Natd:Nat⊢ R a b → R c b → R d c → R a d All goals completed! 🐙

When grind discovers that R a b and R c b hold, E-matching triggers Rsymm to derive R b c, then Rtrans chains the results. For theorems that do not fit any built-in idiom, the grind_pattern command allows manual specification of patterns, including multi-patterns that require all components to match simultaneously before the theorem is instantiated.

3.3. Instantiation constraints🔗

Consider the theorem stating that left-shift distributes over addition in the exponent:

theorem shiftLeft_add (m n : Nat) : ∀ k, m <<< (n + k) = (m <<< n) <<< k := m:Natn:Nat⊢ ∀ (k : Nat), m <<< (n + k) = m <<< n <<< k m:Natn:Natk:Nat⊢ m <<< (n + k) = m <<< n <<< k; All goals completed! 🐙 grind_pattern shiftLeft_add => m <<< (n + k) where m =/= 0

The constraint m =/= 0 prevents instantiation when m is definitionally equal to zero, since the separate theorem zero_shiftLeft (stating 0 \lll n = 0) already covers that case. Without the constraint, grind would generate redundant instances. Other available constraints include generation bounds, instance count limits, structural conditions on matched terms (e.g., requiring a term to be ground or a value), and guards that postpone instantiation until a proposition is known to hold.

3.4. Case splitting and inductive predicates🔗

grind does not case-split over arbitrary Boolean variables like a SAT solver. Instead, it follows structure: splitting on if-then-else expressions, match expressions, and inductive predicates. For inductive predicates, the annotation [grind] enables both case analysis on hypotheses and introduction using the constructors. As an example, we define big-step operational semantics for a simple imperative language.

abbrev Variable := String def State := Variable → Nat inductive Stmt : Type where | skip : Stmt | assign : Variable → (State → Nat) → Stmt | seq : Stmt → Stmt → Stmt | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt | whileDo : (State → Prop) → Stmt → Stmt infix:60 ";; " => Stmt.seq export Stmt (skip assign seq ifThenElse whileDo) set_option quotPrecheck false in notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v) inductive BigStep : Stmt → State → State → Prop where | skip (s : State) : BigStep skip s s | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s]) | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) : BigStep (S;; T) s u | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) : BigStep (ifThenElse B S T) s t | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) : BigStep (ifThenElse B S T) s t | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) : BigStep (whileDo B S) s u | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t attribute [grind] BigStep theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := B:State → PropS:StmtT:Stmts:Statet:State⊢ (ifThenElse B S T,s) ==> t ↔ B s ∧ (S,s) ==> t ∨ ¬B s ∧ (T,s) ==> t All goals completed! 🐙

Here grind case-splits on the BigStep constructors to decompose the hypothesis, propagates the condition B s or its negation into the congruence closure module, and applies the if_true and if_false constructors to close each branch.

3.5. Dependent pattern matching🔗

When match-expressions involve indexed inductive families, the Calculus of Inductive Constructions requires unifying type indices and inserting cast operations---features with no counterpart in first-order or higher-order logic. Consider a function on length-indexed vectors:

inductive Vec (α : Type u) : Nat → Type u | nil : Vec α 0 | cons : α → Vec α n → Vec α (n+1) @[grind =] def Vec.head : Vec α (n+1) → α | .cons a _ => a example (as bs : Vec Int (n+1)) : as.head = bs.head → (match as, bs with | .cons a _, .cons b _ => a + b) = 2 * as.head := n:Natas:Vec Int (n + 1)bs:Vec Int (n + 1)⊢ as.head = bs.head → (match as, bs with | Vec.cons a a_1, Vec.cons b a_2 => a + b) = 2 * as.head All goals completed! 🐙

Because the index is n+1, both arguments must be .cons---the .nil case is ruled out by the type---so Vec.head and the inline match each have a single branch instead of two and four respectively. When grind splits on the match, it generates heterogeneous equalities and cast operations that the E-graph tracks automatically. With only one case surviving, the E-graph learns as = .cons a as' and bs = .cons b bs'; E-matching then instantiates the equation for Vec.head, yielding as.head = a and bs.head = b. Combined with the hypothesis as.head = bs.head, the linear arithmetic solver closes the goal.

4. Typeclass-Parametrized Solvers🔗

SMT solvers such as CVC5  (Barbosaet al, 2022)Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar, 2022. “cvc5: A Versatile and Industrial-Strength SMT Solver”. In Proc. TACAS 2022, LNCS 13243. and Z3  (de Moura and Bjørner, 2008)Leonardo de Moura and Nikolaj Bjørner, 2008. “Z3: An Efficient SMT Solver”. In Proc. TACAS 2008, LNCS 4963. ship built-in theories for a fixed set of types---typically the integers, rationals, and reals, with fixed signatures for +, \times, \leq. Extending them to new types requires modifications to the solver's source code. In grind, each satellite solver is parameterized by Lean typeclasses. The solver activates automatically for any type that provides the required instances---no source-code changes are needed.

4.1. The ring solver🔗

The ring solver reduces polynomial equalities using Gröbner bases. It activates for any type that is at least a commutative semiring, with extensions for commutative rings and fields. The following example derives the value of the fourth power sum from the first three:

open Lean Grind in example [CommRing α] (a b c : α) : a + b + c = 3 → a^2 + b^2 + c^2 = 5 → a^3 + b^3 + c^3 = 7 → a^4 + b^4 + c^4 = 9 := α:Type u_1inst✝:CommRing αa:αb:αc:α⊢ a + b + c = 3 → a ^ 2 + b ^ 2 + c ^ 2 = 5 → a ^ 3 + b ^ 3 + c ^ 3 = 7 → a ^ 4 + b ^ 4 + c ^ 4 = 9 All goals completed! 🐙

Because the solver is parameterized by a typeclass rather than hardcoded for a specific type, the same reasoning applies to any commutative ring. When the ring has a known characteristic p, the solver performs coefficient arithmetic modulo p via the IsCharP typeclass. For example, BitVec 8 is a commutative ring of characteristic 256, and grind handles it without any bitvector-specific theory:

example (x : BitVec 8) : (x - 16) * (x + 16) = x^2 := x:BitVec 8⊢ (x - 16) * (x + 16) = x ^ 2 All goals completed! 🐙

This holds because 16 \times 16 = 256 \equiv 0 \pmod{256}. The ring solver also handles commutative semirings---where subtraction is not available---by constructing the Grothendieck completion to obtain a ring:

open Lean Grind in example [CommSemiring α] [AddRightCancel α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := α:Type u_1inst✝¹:CommSemiring αinst✝:AddRightCancel αx:αy:α⊢ x ^ 2 * y = 1 → x * y ^ 2 = y → y * x = 1 All goals completed! 🐙

4.2. Linear arithmetic and orders🔗

The linear arithmetic solver handles any type equipped with a NatModule (an additive commutative monoid with scalar multiplication by natural numbers) or an IntModule (an additive commutative group with scalar multiplication by integers). It extends naturally to ordered settings---supporting preorders, partial orders, and linear orders---and has further extensions for semirings, rings, and fields. A second solver, lia, implements a CutSat-style  (Jovanović and de Moura, 2013)Dejan Jovanović and Leonardo de Moura (2013). “Cutting to the Chase: Solving Linear Integer Arithmetic”. Journal of Automated Reasoning.51 1pp. 79–108. decision procedure for linear integer arithmetic. It operates over any type that admits an injection into \mathbb{Z} via the ToInt typeclass. For example, UInt32 maps into the range [0, 2^{32}):

example (a b : UInt32) : a ≤ 2 → b ≤ 3 → a + b ≤ 5 := a:UInt32b:UInt32⊢ a ≤ 2 → b ≤ 3 → a + b ≤ 5 All goals completed! 🐙

A dedicated solver for partial and linear orders propagates transitivity, antisymmetry, and totality. It activates for any type with at least a preorder:

open Lean Grind in example [LE α] [Std.IsLinearPreorder α] (a b c d : α) : a ≤ b → ¬ (c ≤ b) → ¬ (d ≤ c) → a ≤ d := α:Type u_1inst✝¹:LE αinst✝:Std.IsLinearPreorder αa:αb:αc:αd:α⊢ a ≤ b → ¬c ≤ b → ¬d ≤ c → a ≤ d All goals completed! 🐙

4.3. Theory combination🔗

The satellite solvers do not operate in isolation. They share information through the congruence closure core: when one solver reports an equality, all solvers see it. The following example requires the ring solver and congruence closure to cooperate. The typeclass NoNatZeroDivisors provides the property that k \neq 0 \land k \cdot a = 0 \implies a = 0, which the ring solver uses for equality propagation:

open Lean Grind in 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 := α: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 All goals completed! 🐙

Here the ring solver derives a^4 + b^4 = 9 - c^4. Congruence closure then deduces f (a^4 + b^4) = f (9 - c^4), reducing the goal to 2 \cdot f(9 - c^4) \neq 1, which is discharged by the linear integer arithmetic solver.

4.4. Extensibility🔗

Built-in solvers are implemented through the same plugin interface that is available to users. A solver extension declares an internalizer (called when new terms enter the E-graph), and equality handlers (called when new equalities and disequalities are discovered). Because the interface is defined in Lean, users can add domain-specific solvers without leaving the language and without any privileged access to grind's internals.

5. Interactive Mode and Diagnostics🔗

When grind fails, or when a user wants to understand or control its behavior, the syntax grind => exposes a domain-specific language for stepping through the solver's execution. Users can invoke individual solver steps, trigger E-matching, perform case splits, inspect equivalence classes, and add new hypotheses---all inside Lean, freely mixing grind steps with ordinary tactic proofs.

grind? outputs a self-contained tactic script containing the exact steps used to close the goal. The generated script does not depend on the annotations from the environment, improving proof stability across library updates. In the following example, grind? generated a script with two steps. The first step instantiates only the theorem trig_identity, and the second applies the ring solver.

axiom Real' : Type noncomputable declaration uses `sorry`instance : Lean.Grind.CommRing Real' := sorry axiom cos : Real' → Real' axiom sin : Real' → Real' axiom trig_identity : ∀ x, (cos x)^2 + (sin x)^2 = 1 -- Manually specify the patterns for `trig_identity` grind_pattern trig_identity => cos x grind_pattern trig_identity => sin x example (x : Real') : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := x:Real'⊢ (cos x + sin x) ^ 2 = 2 * cos x * sin x + 1 grind => x:Real'h✝:¬(cos x + sin x) ^ 2 = 2 * cos x * sin x + 1⊢ False All goals completed! 🐙

6.1. External provers🔗

Sledgehammer  (Paulson and Blanchette, 2010)Lawrence C. Paulson and Jasmin Christian Blanchette, 2010. “Three Years of Experience with Sledgehammer, a Practical Link Between Automatic and Interactive Theorem Provers”. In Proc. IWIL 2010. pioneered the hammer approach for Isabelle/HOL, translating goals to first-order logic and invoking external ATPs (E, Vampire) and SMT solvers (CVC5, Z3). CoqHammer  (Czajka and Kaliszyk, 2018)Łukasz Czajka and Cezary Kaliszyk (2018). “Hammer for Coq: Automation for Dependent Type Theory”. Journal of Automated Reasoning.61 pp. 423–453. adapted this for Coq. In Lean 4, lean-auto  (Qianet al, 2025)Yicheng Qian, Joshua Clune, Clark Barrett, and Jeremy Avigad, 2025. “Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers”. In Computer Aided Verification. translates goals to monomorphic higher-order logic and dispatches to external ATPs, while LeanHammer  (Zhuet al, 2025)Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, and Sean Welleck, 2025. “Premise Selection for a Lean Hammer”. arXiv:2506.07477 adds neural premise selection. lean-smt  (Mohamedet al, 2025)Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, and Clark Barrett, 2025. “lean-smt: An SMT Tactic for Discharging Proof Goals in Lean”. In Proc. CAV 2025, LNCS 15933. and SMTCoq  (Ekiciet al, 2017)Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark Barrett, 2017. “SMTCoq: A Plug-in for Integrating SMT Solvers into Coq”. In Proc. CAV 2017, LNCS 10427. integrate external SMT solvers with Lean 4 and Coq respectively, reconstructing proofs from solver certificates. These tools benefit from mature premise selection and highly optimized solver backends, making them more scalable when large numbers of lemmas are available. The cost is a translation gap: not every feature of the Calculus of Inductive Constructions has a counterpart in the target logic, reconstruction can fail even when the external prover succeeds, and the round-trip adds latency. grind avoids all three costs by operating directly on Lean expressions and producing kernel-checkable proof terms incrementally. Because it runs inside the Lean elaborator, verification frameworks built in Lean---such as Aeneas  (Ho and Protzenko, 2022)Son Ho and Jonathan Protzenko (2022). “Aeneas: Rust Verification by Functional Translation”. Proc. ACM Program. Lang.6 ICFPpp. 711–741. and Velvet  (Gladshteinet al, 2026)Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey (2026). “Foundational Multi-Modal Program Verifiers”. Proc. ACM Program. Lang.10 POPL.---can share state across grind calls: E-graph contents, resolved instances, and asserted facts carry over when multiple verification conditions share a common proof context.

6.2. Automation in Lean 4🔗

In Lean 4, the simp tactic performs equational rewriting. The omega tactic decides Presburger arithmetic over Nat and Int. Aesop  (Limperg and From, 2023)Jannis Limperg and Asta Halkjær From, 2023. “Aesop: White-Box Best-First Proof Search for Lean”. In Proc. CPP 2023. performs best-first search over tactic scripts. Canonical  (Norman and Avigad, 2025)Chase Norman and Jeremy Avigad, 2025. “Canonical for Automated Theorem Proving in Lean”. In Proc. ITP 2025, LIPIcs 352. is a type inhabitation solver that exhaustively searches for proof terms in a canonical form. The egg tactic  (Rosselet al, 2026)Marcus Rossel, Rudi Schneider, Thomas Koehler, Michel Steuwer, and Andrés Goens (2026). “Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation”. Proc. ACM Program. Lang.10 POPLpp. 718–747. uses equality saturation to explore the space of equivalent terms via e-graphs, similar to grind's directed congruence closure. grind complements these: it combines theory reasoning with E-matching in a single framework, handles algebraic structures through typeclasses, and supports user extensibility through the plugin API and the constraint propagator interface.

7. Evaluation and Conclusion🔗

grind was released in August 2025 and has been rapidly adopted. As of February 2026, Mathlib uses grind approximately 3,400 times across 2,400 theorems. Of these, around 1,200 were initially authored using grind, while the other 1,200 were refactored after grind became available. These refactors averaged a reduction of 28% in lines of code, with ~50 theorems seeing proofs reduced by 10 lines or more (analysis script). CSLib  (Barrettet al, 2026)Clark Barrett, Swarat Chaudhuri, Fabrizio Montesi, Jim Grundy, Pushmeet Kohli, Leonardo de Moura, Alexandre Rademaker, and Sorrachai Yingchareonthawornchai, 2026. “CSLib: The Lean Computer Science Library”. arXiv:2602.04846, the Prime Number Theorem project and Terence Tao's Analysis I repository each also uses grind around 500 times.

The most immediate opportunities lie in scaling premise selection to large unannotated libraries. We already have a configurable premise selection engine (grind +suggestions), which uses trigger-based relevance filtering inspired by Hoder and Voronkov (2011)Kryštof Hoder and Andrei Voronkov, 2011. “Sine Qua Non for Large Theory Reasoning”. In Proc. CADE-23, LNAI 6803. to rank unannotated library theorems by relevance to the current goal, but it needs tuning for Lean's libraries, and we anticipate integrating external neural premise selection engines. We also plan to scale better when very large (>1000) numbers of lemmas are available for instantiation, and have initial linting tools to help users design good annotations.

7.1. Disclosure of Interests🔗

The authors have no competing interests to declare that are relevant to the content of this article.