# The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

arXiv: https://arxiv.org/abs/2512.07087 · HTML: https://mlsanity.com/paper/2512.07087/

## Key facts

- Cited by 10 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Dec 2025.

## Built on by (most cited first, 10 of 10)

- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [DIVE: Unlocking Self-Improvement in Frozen Language Models Through Diversity-Driven Skill Evolution](https://mlsanity.com/paper/2608.12486/) (2026)
- [Discovering mathematical concepts through a multi-agent system](https://mlsanity.com/paper/2603.04528/) (2026)
- [ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction](https://mlsanity.com/paper/2608.15979/) (2026)
- [A Certificate-Producing Cascade for Equational Implication: The SAIR EQT2 Stage 2 Solver](https://mlsanity.com/paper/2609.00706/) (2026)
- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)
- [NanoProof: Open and Efficient Automated Theorem Proving in Lean 4](https://mlsanity.com/paper/2610.11605/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.