The equational theories project: Advancing collaborative mathematical research at scale
Bolan M, Breitner J, Brox J, Carlini N, Carneiro M, Doorn F van, Dvorak M, Goens A, Hill A, Husum H, Mejia HI, Kocsis ZA, Floch BL, Bar-on A, Luccioli L, McNeil D, Meiburg A, Monticone P, Nielsen PP, Osazuwa EO, Paolini G, Petracci M, Reinke B, Renshaw D, Rossel M, Roux C, Scanvic J, Srinivas S, Tadipatri AR, Tao T, Tsyrklevich V, Vaquerizo-Villar F, Weber D, Zheng F. The equational theories project: Advancing collaborative mathematical research at scale. arXiv, 10.48550/arXiv.2512.07087.
Download (ext.)
Preprint
| Submitted
| English
Author
Bolan, Matthew;
Breitner, Joachim;
Brox, Jose;
Carlini, Nicholas;
Carneiro, Mario;
Doorn, Floris van;
Dvorak, MartinISTA 
;
Goens, Andrés;
Hill, Aaron;
Husum, Harald;
Mejia, Hernán Ibarra;
Kocsis, Zoltan A.
All
;
Goens, Andrés;
Hill, Aaron;
Husum, Harald;
Mejia, Hernán Ibarra;
Kocsis, Zoltan A.
All
Department
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.
Publishing Year
Date Published
2025-12-16
Journal Title
arXiv
IST-REx-ID
Cite this
Bolan M, Breitner J, Brox J, et al. The equational theories project: Advancing collaborative mathematical research at scale. arXiv. doi:10.48550/arXiv.2512.07087
Bolan, M., Breitner, J., Brox, J., Carlini, N., Carneiro, M., Doorn, F. van, … Zheng, F. (n.d.). The equational theories project: Advancing collaborative mathematical research at scale. arXiv. https://doi.org/10.48550/arXiv.2512.07087
Bolan, Matthew, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, et al. “The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale.” ArXiv, n.d. https://doi.org/10.48550/arXiv.2512.07087.
M. Bolan et al., “The equational theories project: Advancing collaborative mathematical research at scale,” arXiv. .
Bolan M, Breitner J, Brox J, Carlini N, Carneiro M, Doorn F van, Dvorak M, Goens A, Hill A, Husum H, Mejia HI, Kocsis ZA, Floch BL, Bar-on A, Luccioli L, McNeil D, Meiburg A, Monticone P, Nielsen PP, Osazuwa EO, Paolini G, Petracci M, Reinke B, Renshaw D, Rossel M, Roux C, Scanvic J, Srinivas S, Tadipatri AR, Tao T, Tsyrklevich V, Vaquerizo-Villar F, Weber D, Zheng F. The equational theories project: Advancing collaborative mathematical research at scale. arXiv, 10.48550/arXiv.2512.07087.
Bolan, Matthew, et al. “The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale.” ArXiv, doi:10.48550/arXiv.2512.07087.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Link(s) to Main File(s)
Access Level
Open Access
Export
Marked PublicationsOpen Data ISTA Research Explorer
Sources
arXiv 2512.07087
Google Scholar