Reference. 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 A. 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, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, Fan Zheng · arXiv · 2025 · DOI · 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.

Cite
Cite as @bolan-2025-the (helia, typst) · \cite{bolan-2025-the} (LaTeX)
BibTeX
bibtex · 10 lines
@misc{bolan-2025-the,
  doi = {10.48550/ARXIV.2512.07087},
  url = {https://arxiv.org/abs/2512.07087},
  author = {Bolan, Matthew and Breitner, Joachim and Brox, Jose and Carlini, Nicholas and Carneiro, Mario and van Doorn, Floris and Dvorak, Martin and Goens, Andrés and Hill, Aaron and Husum, Harald and Mejia, Hernán Ibarra and Kocsis, Zoltan A. and Floch, Bruno Le and Bar-on, Amir Livne and Luccioli, Lorenzo and McNeil, Douglas and Meiburg, Alex and Monticone, Pietro and Nielsen, Pace P. and Osazuwa, Emmanuel Osalotioman and Paolini, Giovanni and Petracci, Marco and Reinke, Bernhard and Renshaw, David and Rossel, Marcus and Roux, Cody and Scanvic, Jérémy and Srinivas, Shreyas and Tadipatri, Anand Rao and Tao, Terence and Tsyrklevich, Vlad and Vaquerizo-Villar, Fernando and Weber, Daniel and Zheng, Fan},
  keywords = {Rings and Algebras (math.RA), Logic in Computer Science (cs.LO), FOS: Mathematics, FOS: Mathematics, FOS: Computer and information sciences, FOS: Computer and information sciences},
  title = {The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale},
  publisher = {arXiv},
  year = {2025},
  copyright = {Creative Commons Attribution 4.0 International}
}
hayagriva YAML (typst)
yaml · 45 lines
bolan-2025-the:
  type: misc
  title: 'The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale'
  author:
  - Bolan, Matthew
  - Breitner, Joachim
  - Brox, Jose
  - Carlini, Nicholas
  - Carneiro, Mario
  - name: Doorn
    given-name: Floris
    prefix: van
  - Dvorak, Martin
  - Goens, Andrés
  - Hill, Aaron
  - Husum, Harald
  - Mejia, Hernán Ibarra
  - Kocsis, Zoltan A.
  - Floch, Bruno Le
  - Bar-on, Amir Livne
  - Luccioli, Lorenzo
  - McNeil, Douglas
  - Meiburg, Alex
  - Monticone, Pietro
  - Nielsen, Pace P.
  - Osazuwa, Emmanuel Osalotioman
  - Paolini, Giovanni
  - Petracci, Marco
  - Reinke, Bernhard
  - Renshaw, David
  - Rossel, Marcus
  - Roux, Cody
  - Scanvic, Jérémy
  - Srinivas, Shreyas
  - Tadipatri, Anand Rao
  - Tao, Terence
  - Tsyrklevich, Vlad
  - Vaquerizo-Villar, Fernando
  - Weber, Daniel
  - Zheng, Fan
  date: 2025
  publisher: arXiv
  url: https://arxiv.org/abs/2512.07087
  serial-number:
    doi: 10.48550/ARXIV.2512.07087
Download: bolan-2025-the.bib · bolan-2025-the.yml
Cites 68 works (1 here)
With notes (1)

egg: Fast and Extensible Equality Saturation willsey-2021-eggPOPL · 2021
An e-graph efficiently represents a congruence relation over many expressions. Although they were originally developed in the late 1970s for use in automated theorem provers, a more recent technique known as equality saturation repurposes e-graphs to implement state-of-the-art, rewrite-driven compiler optimizations and program synthesizers. However, e-graphs remain unspecialized for this newer use case. Equality saturation workloads exhibit distinct characteristics and often require ad-hoc e-graph extensions to incorporate transformations beyond purely syntactic rewrites. This work contributes two techniques that make e-graphs fast and extensible, specializing them to equality saturation. A new amortized invariant restoration technique called rebuilding takes advantage of equality saturation’s distinct workload, providing asymptotic speedups over current techniques in practice. A general mechanism called e-class analyses integrates domain-specific analyses into the e-graph, reducing the need for ad hoc manipulation. We implemented these techniques in a new open-source library called egg. Our case studies on three previously published applications of equality saturation highlight how egg’s performance and flexibility enable state-of-the-art results across diverse domains.
PDF · DOI · arXiv · pldb
External (67)
bolan-2025-the reference entries/refs/bolan-2025-the/bolan-2025-the.hel