eqtheory

A Python library for equational theories over magmas: given two equations in one binary operation ◇, decide whether the first implies the second — and hand back a Lean 4 certificate either way.

• term rewriting with a ground Knuth–Bendix order, one-way matching, unification,
• a proof-producing e-graph (congruence closure with a proof forest, shortest shared explanations) and equality saturation,
• ordered completion and goal-directed superposition with replayed proof chains, interreduction and node budgets,
• finite countermodels: symbolic linear families, structured tables, a complete propagating cell search and a CDCL SAT search with symmetry breaking (exhaustion verdicts are proofs),
• infinite countermodels on ℕ for Austin pairs (true in every finite magma, false in general),
• Lean 4 certificates for every answer, in the shapes accepted by the SAIR Stage-2 judge, with an optional compile check,
• an optional, hygienic LLM stage with a configurable prompt,
• a CLI with e-graph and proof visualisation (SVG/PNG/DOT).

The algorithms are those of the SAIR Stage-2 solver (800/800 practice, see the paper in osick/SAIR-callenges), re-packaged with a clean API. Pure Python 3.11+, no required dependencies.

pip install -e .            # from this directory
pip install -e ".[viz,dev]" # graphviz bindings, pytest

Quick start

from eqtheory import Problem, solve

p = Problem.parse("x = y ◇ (x ◇ y)", "x = (x ◇ y) ◇ x")
ans = solve(p)
print(ans.verdict, ans.stage)   # "true" / "false", which engine decided
print(ans.code)                 # the Lean 4 certificate

Each engine is a plain function:

from eqtheory import prove_by_superposition, find_countermodel, residue_affine_countermodel, prove_goal
from eqtheory.lean import certs

pr = prove_by_superposition(p.hypothesis, p.goal)       # lemma + instantiation + derived set
cm = find_countermodel(p.hypothesis, p.goal, time_budget=60)   # Countermodel(n, table) or None
nm = residue_affine_countermodel(p.hypothesis, p.goal)  # ℕ model for Austin pairs
eg, l, r = prove_goal(p.hypothesis, p.goal)             # e-graph with the goal sides merged
lemmas, chain = eg.explain(l, r)                        # shared proof, replayable
eg.render("egraph.svg", highlight=(l, r))               # picture

Command line

eqtheory solve "x = y ◇ (x ◇ y)" "x = (x ◇ y) ◇ x"                # full ladder, prints certificate
eqtheory solve --lean --json ...                                # certificate compiled with Lean
eqtheory prove ...                                              # superposition only
eqtheory model --infinite --cert ...                            # countermodels, finite then ℕ
eqtheory egraph --render egraph.svg --lemmas ...                # saturate and draw the e-graph
eqtheory viz-proof --out proof.dot ...                          # the extracted proof as a graph
eqtheory cert --table "[[0,1],[1,0]]" ...                       # wrap a table as a certificate

--lean needs EQTHEORY_LEAN_BIN (a Lean 4.33 binary) and EQTHEORY_JUDGE_ROOT (a built checkout of the Stage-2 judge library) or EQTHEORY_LEAN_PATH. --llm needs OPENROUTER_API_KEY.

Documentation

• User guide — the pipeline, budgets, composing your own ladder
• Mathematical background — the theory behind each engine, with references
• Certificates — the Lean shapes and the proof-policy lessons
• API overview
• Limitations — theoretical and pragmatic
• Releasing — moving to its own repository, CI, tags, PyPI
• examples/single_file_solver.py — a complete solver in 60 lines
• artifacts/ — sample renderings and benchmark reports

Status

Version 0.1.0 (2026-09-01). Tests: python -m pytest (70 tests; the Lean end-to-end test is skipped unless Lean is configured). Benchmark (2026-09-01, 200-problem Stage-2 stress set, every certificate compiled with Lean, LLM never needed): 200/200 correct — see artifacts/bench-stress-2026-09-01/REPORT.md.

Limitations (short form)

Implication between magma laws is undecidable; every engine is budgeted, so "no answer" is not a verdict. Finite search is complete per size but cannot see infinite-only countermodels beyond the ℕ residue-class family; table certificates stop at Fin 10 (affine models go further); grind certificates are Lean-version-sensitive; the compile check is not the competition judge; the LLM stage adds hygiene, not reach. Details and measurements: docs/limitations.md.

License: MIT.