The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Authors
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
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.
