The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

TL;DR

The paper documents the Equational Theories Project (ETP), a large-scale, crowdsourced, machine-assisted mathematical collaboration aimed at fully mapping the implication graph among 4694 equational laws for magmas, with all results formalized in Lean. It combines human insight, diverse automated theorem provers, and rigorous software tooling to produce a complete 22,033,636-edge graph (and a finite-variant graph), organized into equivalence classes and accompanied by extensive counterexamples and algebraic constructions. Beyond the central result, the work presents a detailed workflow for scalable formalization, including blueprint-driven planning, task automation, and robust data/visualization interfaces, and it documents numerous methodological advances in counterexample construction, syntactic reasoning, and proof reconstruction. The project demonstrates that large-scale, formally verified mathematical investigations are feasible with a modular, tool-supported collaboration model and suggests promising directions for extending these methods to richer logical relations and higher-order law classes. Overall, ETP provides a comprehensive blueprint for future data-driven, AI-assisted mathematical collaboration at scale with practical benchmarks and open questions for finite-model and spectrum analyses.

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.

Figures (16)

• Figure 1: A Hasse diagram of all the equational laws implied by $\mathrm{E}854$ (for unrestricted magmas). An edge in this diagram indicates that the lower equation implies the higher one. Rounded rectangles indicate groups of equivalent laws. This graph was produced by the visualization tool Graphiti, which was developed for this project.
• Figure 2: A Hasse diagram of all the equational laws implied by $\mathrm{E}1729$, both for unrestricted magmas (left) and finite magmas (right). Note the slightly larger number of implications in the latter.
• Figure 3: Longest chains of implications (length $15$) between inequivalent laws in the implication graph. The parts above/below law $\mathrm{E}3$ can be independently dualized.
• Figure 4: Some of the main dynamics in which proofs were generated, discussed within the Lean Zulip channel and then formalized in the GitHub repository. Boldface arrows indicate human activities, such as proposing an automated attack on outstanding implications, converting a computer-generated proof into a human-readable format, formalizing a human readable proof directly, or first creating a more precise blueprint for other collaborators to work on. Dashed arrows indicate fully automated processes, while the partly dashed line indicates a semi-automated process requiring human supervision.
• Figure 5: A sample proof of a formalized implication, in this case that $\mathrm{E}1437 \not\models \mathrm{E}4269$.

Theorems & Definitions (43)

• Example 2.1: Commutative and associative free magma
• Example 2.2: Left-absorptive free magma
• Remark 4.1
• Remark 5.1
• Example 5.2: Commutative counterexample
• Example 5.3: Noncommutative counterexample
• Remark 5.4
• Remark 5.5
• Remark 5.6
• Example 5.7: Abelian example