RT info:eu-repo/semantics/article
T1 The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
A1 Brox López, José Ramón
A1 Tao, Terence
A1 Bolan, Matthew
A1 Breitner, Joachim
A1 Carlini, Nicholas
A1 Carneiro, Mario
A1 van Doorn, Floris
A1 Dvorak, Martin
A1 Goens, Andrés
A1 Hill, Aaron
A1 Husum, Harald
A1 Ibarra Mejía, Hernán
A1 Kocsis, Zoltan
A1 Le Floch, Bruno
A1 Livne Bar-on, Amir
A1 Luccioli, Lorenzo
A1 McNeil, Douglas
A1 Meiburg, Alex
A1 Monticone, Pietro
A1 Nielsen, Pace P.
A1 Osalotioman Osazuwa, Emmanuel
A1 Paolini, Giovanni
A1 Petracci, Marco
A1 Reinke, Bernhard
A1 Renshaw, David
A1 Rossel, Marcus
A1 Roux, Cody
A1 Scanvic, Jérémy
A1 Srinivas, Shreyas
A1 Tadipatri, Anand Rao
A1 Tsyrklevich, Vlad
A1 Vaquerizo Villar, Fernando
A1 Weber, Daniel
A1 Zheng, Fan
K1 Álgebra universal
K1 Inteligencia artificial
K1 Demostración automática de teoremas
K1 Formalización de las matemáticas
K1 Matemáticas colaborativas
K1 Teoría de grupos
K1 Álgebra universal
K1 Inteligencia artificial
K1 Demostración automática de teoremas
K1 Formalización de las matemáticas
K1 Matemáticas colaborativas
K1 Magmas
K1 Identidades polinómicas
K1 Vampire
K1 Prover9-Mace4
K1 Lean
K1 GitHub
K1 Teoría de grupos
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.
PB arXiv
YR 2025
FD 2025-12-08
LK https://uvadoc.uva.es/handle/10324/80484
UL https://uvadoc.uva.es/handle/10324/80484
LA eng
NO arXiv:2512.07087
NO Producción Científica
DS UVaDOC
RD 12-ene-2026