The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Rings and Algebras
2025-12-17 v2 Logic in Computer Science
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.
Cite
@article{arxiv.2512.07087,
title = {The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale},
author = {Matthew Bolan and Joachim Breitner and Jose Brox and Nicholas Carlini and Mario Carneiro and Floris van Doorn and Martin Dvorak and Andrés Goens and Aaron Hill and Harald Husum and Hernán Ibarra Mejia and Zoltan A. Kocsis and Bruno Le Floch and Amir Livne Bar-on and Lorenzo Luccioli and Douglas McNeil and Alex Meiburg and Pietro Monticone and Pace P. Nielsen and Emmanuel Osalotioman Osazuwa and Giovanni Paolini and Marco Petracci and Bernhard Reinke and David Renshaw and Marcus Rossel and Cody Roux and Jérémy Scanvic and Shreyas Srinivas and Anand Rao Tadipatri and Terence Tao and Vlad Tsyrklevich and Fernando Vaquerizo-Villar and Daniel Weber and Fan Zheng},
journal= {arXiv preprint arXiv:2512.07087},
year = {2025}
}
Comments
74 pages; https://teorth.github.io/equational_theories/ swh:1:dir:426b52ba40033a37c18474ef44068e23c55df4bc