The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

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. Some examples of equational laws, together with the number that we assigned to that law, include

Up to relabeling and symmetry, there turn out to be 4694 equational laws that involve at most four invocations of the magma operation ; one can explore them in our “Equation Explorer” tool.

The aim of the project was to work out which of these laws imply which others. For instance, all laws imply the trivial law , and conversely the singleton law implies all the others. On the other hand, the commutative law does not imply the associative law (because there exist magmas that are commutative but not associative), nor is the converse true. All in all, there are implications of this type to settle; most of these are relatively easy and could be resolved in a matter of minutes by an expert in college-level algebra, but prior to this project, it was impractical to actually do so in a manner that could be feasibly verified. Also, this problem is known to become undecidable for sufficiently long equational laws. Nevertheless, we were able to resolve all the implications informally after two months, and have them completely formalized in Lean after a further five months.

After a rather hectic setup process (documented in this personal log), progress came in various waves. Initially, huge swathes of implications could be resolved first by very simple-minded techniques, such as brute-force searching all small finite magmas to refute implications; then, automated theorem provers such as Vampire or Mace4 / Prover9 were deployed to handle a large fraction of the remainder. A few equations had existing literature that allowed for many implications involving them to be determined. This left a core of just under a thousand implications that did not fall to any of the “cheap” methods, and which occupied the bulk of the efforts of the project. As it turns out, all of the remaining implications were negative; the difficulty was to construct explicit magmas that obeyed one law but not another. To do this, we discovered a number of general constructions of magmas that were effective at this task. For instance:

• Linear models, in which the carrier was a (commutative or noncommutative) ring and the magma operation took the form for some coefficients , turned out to resolve many cases.
• We discovered a new invariant of an equational law, which we call the “twisting semigroup” of that law, which also allowed us to construct further examples of magmas that obeyed one law but not another , by starting with a base magma that obeyed both laws, taking a Cartesian power of that magma, and then “twisting” the magma operation by certain permutations of designed to preserve but not .
• We developed a theory of “abelian magma extensions”, similar to the notion of an abelian extension of a group, which allowed us to flexibly build new magmas out of old ones in a manner controlled by a certain “magma cohomology group ” which were tractable to compute, and again gave ways to construct magmas that obeyed one law but not another .
• Greedy methods, in which one fills out an infinite multiplication table in a greedy manner (somewhat akin to naively solving a Sudoku puzzle), subject to some rules designed to avoid collisions and maintain a law , as well as some seed entries designed to enforce a counterexample to a separate law . Despite the apparent complexity of this method, it can be automated in a manner that allowed for many outstanding implications to be refuted.
• Smarter ways to utilize automated theorem provers, such as strategically adding in additional axioms to the magma to help narrow the search space, were developed over the course of the project.

Even after applying all these general techniques, though, there were about a dozen particularly difficult implications that resisted even these more powerful methods. Several ad hoc constructions were needed in order to understand the behavior of magmas obeying such equations as E854, E906, E1323, E1516, and E1729, with the latter taking months of effort to finally solve and then formalize.

A variety of GUI interfaces were also developed to facilitate the collaboration (most notably the Equation Explorer tool mentioned above), and several side projects were also created within the project, such as the exploration of the implication graph when the magma was also restricted to be finite. In this case, we resolved all of the implications except for one (and its dual):

Problem 1 Does the law (E677) imply the law (E255) for finite magmas?

See this blueprint page for some partial results on this problem, which we were unable to resolve even after months of effort.

Interestingly, modern AI tools did not play a major role in this project (but it was largely completed in 2024, before the most recent advanced models became available); while they could resolve many implications, the older “good old-fashioned AI” of automated theorem provers were far cheaper to run and already handled the overwhelming majority of the implications that the advanced AI tools could. But I could imagine that such tools would play a more prominent role in future similar projects.