01E-Graphs
E-graphs compactly represent large spaces of equivalent terms, and they sit at the
core of automated theorem provers, SMT solvers, and optimizing compilers. The
data structure is built around one kind of fact: equality between terms. For
example, the e-graph below contains the atoms a and b and
the applications f(a) and f(b). Rectangles are
e-nodes, one per term; circles are e-classes, the sets of e-nodes
known to be equal; and each arrow connects an e-node to the e-class of its argument.
Initially every e-node sits in its own e-class (a). Asserting a = b
merges their e-classes (b), and by congruence the e-graph discovers on its own that
f(a) = f(b), merging those e-classes as well (c).
That last step is the whole point, and it is also where the obligations live. An e-graph is only useful if it denotes exactly the congruence closure of the equalities asserted into it: no fewer equalities, or the tool built on it is incomplete; no more, or it is unsound. Between assertions the structure passes through states where its invariants are temporarily broken and later repaired, and the argument that this is safe is a genuine proof, not a remark.
02Why Mechanize
In practice that proof is written on paper, if it is written at all. Implementations then diverge from it: they add deferred rebuilding, analyses attached to e-classes, and scheduling heuristics, each of which perturbs the invariants the paper argument relied on. Checking whether the argument still goes through means redoing it by hand.
The pressure compounds because e-graphs are no longer one data structure but a family. Extensions add disequalities, assumptions and versioning, lattice operations over contexts. Each is published with its own metatheory, and each restates the shared core — terms, e-classes, congruence, the closure argument — before it can say anything new. The interesting content of an extension is small; the scaffolding around it is not.
A mechanization changes the economics. Once the core is machine-checked, an extension refines existing definitions instead of restating them, and the proofs it inherits are reused rather than re-argued. What remains to prove is exactly what is new, and a change to the core is re-checked against every extension at once. LeanGraph builds that core in Lean and grows the family on top of it.