• 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 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, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng, and I have just uploaded to the arXiv our preprint The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. • This is the final report for the Equational Theories Project, which was proposed in this blog post and also showcased in this subsequent blog post. • The aim of this project was to see whether one could collaboratively achieve a large-scale systematic exploration of a mathematical space, which in this case was the implication graph between 4694 equational laws of magmas. • A magma is a set equipped with a binary operation (or, equivalently, a multiplication table). • An equational law is an equation involving this operation and a number of indeterminate variables.
Article Summaries:
- A large‑collaborative team of mathematicians and computer scientists has released the final report of the Equational Theories Project, now posted on arXiv. The project systematically examined the implication graph among 4,694 equational laws governing magmas-sets with a binary operation-using a mix of brute‑force searches, automated theorem provers (Vampire, Mace4, Prover9), literature results, and new magma constructions. Over two months the team resolved all implications, and an additional five months formalized the findings in the Lean proof assistant. The work demonstrates that large‑scale, verifiable exploration of algebraic law relationships is feasible, even for problems that are undecidable in general.
Sources: