The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

TL;DR

The Equational Theories Project demonstrates large-scale collaborative mathematical research using machine-assisted proofs, successfully mapping implications among numerous equational laws on magmas and discovering new algebraic constructions.

Contribution

It introduces a scalable online platform combining human and automated proofs, advancing collaborative exploration in mathematics with formal verification tools.

Findings

Mapped over 22 million implications between laws

Discovered new magma constructions satisfying specific laws

Addressed auxiliary questions on finite magmas

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.