Work in progress

Machine-Checked
E-Graph Theory

E-graphs sit at the core of provers, SMT solvers, and optimizing compilers, and the family of extensions built on them keeps growing. Their metatheory, though, is still argued on paper, and every extension re-argues it from scratch. LeanGraph mechanizes that theory in Lean: definitions, invariants, and correctness proofs, machine-checked once and reused by every extension.

01The Library

  1. 01

    Definitions

    The objects, spelled out: terms and e-nodes, e-classes and the equivalence relation an e-graph denotes, and the congruence closure it is meant to compute. Implementation-independent, so results transfer between concrete e-graph designs.

    Coming soon
  2. 02

    Key Theorems

    The results worth having once and for all: that an e-graph denotes exactly the congruence closure of the equalities asserted into it, that its invariants survive merging and rebuilding, and that saturation terminates.

    Coming soon
  3. 03

    Using It

    LeanGraph is a plain Lean package: add it to your lakefile, import the namespace, and build on the definitions and lemmas directly. No proof obligations are left to the caller beyond the ones stated in the interfaces.

    Coming soon
  4. 04

    Contributing

    The core is meant to be extended. Each extension — disequalities, versioning, and whatever comes next — refines the same definitions and inherits the same proofs, so a new one starts from the invariants instead of restating them.

    Coming soon

Read more →

02Publications

Nothing published yet — papers and artifacts will be listed here as they appear.

03Credits

is developed by the Programming Group at the University of St. Gallen.