The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan A. Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng
math.RA
Dec 8, 2025 · v1
TL;DR
All 22,028,942 implications between 4694 equational laws on magmas were formalized and validated in Lean with Mathlib.
Abstract
We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.
Problem
Determining the implication relationships among equational laws on magmas is a large-scale combinatorial problem: there are 4694 candidate single-operation equational laws and over 22 million potential implications to resolve.
Approach
The Equational Theories Project (ETP) was an online collaborative effort combining human-generated proofs, automated theorem proving (including an egg-based e-graph tactic and Vampire/Prover9), and counterexample constructions via SAT solvers and specialized magma constructions. All results were validated in the Lean proof assistant. The project used a custom dashboard, Lean CI infrastructure, and the Graphiti visualization tool for project management at scale.
Results
The project successfully determined all 22,028,942 edges of the implication graph between 4694 equational laws on magmas. Several new magma constructions were discovered, and auxiliary questions about finite versus infinite magmas were addressed. The project demonstrated a new model for large-scale collaborative formal mathematics.
