The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

@misc{bolan2026equational,
  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 Kocsis and Bruno Le Floch and Amir Livne Bar-On and Lorenzo Luccioli and Douglas Mcneil and Alex Meiburg and Pietro Monticone and Pace 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},
  howpublished = {HAL},
  year = {2026},
  month = nov,
  eprint = {2512.07087},
  archivePrefix = {arXiv},
  url = {https://hal.science/hal-05848442v1},
  note = {CC BY 4.0},
}

TY  - UNPB
TI  - The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
AU  - Matthew Bolan
AU  - Joachim Breitner
AU  - Jose Brox
AU  - Nicholas Carlini
AU  - Mario Carneiro
AU  - Floris van Doorn
AU  - Martin Dvorak
AU  - Andrés Goens
AU  - Aaron Hill
AU  - Harald Husum
AU  - Hernán Ibarra Mejia
AU  - Zoltan Kocsis
AU  - Bruno Le Floch
AU  - Amir Livne Bar-On
AU  - Lorenzo Luccioli
AU  - Douglas Mcneil
AU  - Alex Meiburg
AU  - Pietro Monticone
AU  - Pace Nielsen
AU  - Emmanuel Osalotioman Osazuwa
AU  - Giovanni Paolini
AU  - Marco Petracci
AU  - Bernhard Reinke
AU  - David Renshaw
AU  - Marcus Rossel
AU  - Cody Roux
AU  - Jérémy Scanvic
AU  - Shreyas Srinivas
AU  - Anand Rao Tadipatri
AU  - Terence Tao
AU  - Vlad Tsyrklevich
AU  - Fernando Vaquerizo-Villar
AU  - Daniel Weber
AU  - Fan Zheng
PY  - 2026
DA  - 2026/11/02
PB  - HAL
UR  - https://hal.science/hal-05848442v1
AB  - 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.
ER  -