E-Graphs

For proving implications, we used another technique called equality saturation (Willsey et al. 2021) with the lean-egg tactic, to automatically construct proofs.

A similar approach is being pursued in the MagmaEgg tool as well, which is a standalone program that only supports magma equalities, while the lean-egg tactic supports any Lean expression.

The dependency explorer needs JavaScript and its graph data.