17.2. What is grind?

A proof‑automation tactic inspired by modern SMT solvers.

Picture a virtual white‑board: every time grind discovers a new equality, inequality, or Boolean literal it writes that fact on the board, merges equivalent terms into buckets, and invites each engine to read from—and add back to—the shared white-board. The cooperating engines are:

• congruence closure,

• constraint propagation,

• E‑matching,

• guided case analysis, and

• a suite of satellite theory solvers (linear integer arithmetic, commutative rings, …).

Lean supports dependent types and a powerful type‑class system, and grind produces ordinary Lean proof terms for every fact it adds.