Makes Julia reason with equations. General purpose metaprogramming, symbolic computation and algebraic equational reasoning library for the Julia programming language: E-Graphs & equality saturation, term rewriting and more.

An awesome list of e-graph resources

A toy compiler for NumPy array expressions that uses e-graphs and MLIR

Python bindings for the egglog rust library

Fast equality saturation in Haskell

🚧 Build a SQL optimizer in 1000 lines of Rust using egg.

EGraphs in OCaml

A pure, low-level tensor program representation enabling tensor program optimization via program rewriting. See the web demo at https://gussmith23.github.io/glenside-web-demo/

A language-generic implementation of equality saturation in Haskell

E-Graph library

An egglog-compatible but faster ahead-of-time compiling e-graph engine.

An experimental Differential Dataflow optimization engine powered by equality saturation

Flexible Matching: Explore and reveal accelerator-supported workloads in Deep Learning Models

Equality Saturation Framework for Directive-Based GPU Code

E-graph implementation for educational purposes

Harmony automation tool available through program optimization (e-graphs)

Inference engine for extensional untyped λ-calculus

Differential Refrain Engine — unified time-pattern DSL (egg + autodiff + Loro + cell complex)

Formally verified equality saturation engine in Lean 4 — 248 theorems, zero sorry, zero axioms

Experimental mathematics and symbolic discovery platform for rewrite search, equality saturation, hypothesis mining, counterexample search, proof workflows, and reproducible mathematical exploration.