// the find
teorth/equational_theories
A project to map out the relations between different equational theories of Magmas.
A massively collaborative Lean formalization project, led by Terence Tao, that tries to settle all ~22 million implications between the 4,694 single-equation axioms a magma can satisfy. It's aimed at people interested in formal verification, universal algebra, or how large swarms of contributors (human and automated provers) can crack a huge combinatorial math problem in public.
The project decomposes a genuinely enormous problem into thousands of small, independently checkable Lean lemmas, which is what makes mass collaboration tractable at all. It wires in external automated provers (Vampire, Z3, Prover9, twee) so people can find a proof or counterexample with conventional tools before anyone formalizes it in Lean. The auto-generated dashboard, implication-graph explorer, and finite magma explorer give a live, honest view of what's actually proven versus conjectured rather than just a commit log. The underlying data (equation lists, duals, smallest-magma tables) is plain text/JSON and reusable outside the Lean build entirely.
There's no library surface here — nothing to import or depend on; the only reason to clone it is to contribute proofs or mine the dataset. The blueprint and paper are both marked work-in-progress, and with 22 million implications to resolve this is a multi-year effort with no near-term 'done' state. The commentary directory is thousands of individual per-equation markdown files, which is painful to browse or grep without the website's search tooling. Contributing meaningfully requires real fluency in Lean's tactic language, so the barrier to entry is high despite the inviting framing of 'universal algebra for everyone.'