cff-version: 1.2.0
message: >
  If you use this project in your work, please cite it using the metadata below.
title: "The Equational Theories Project"
version: 0.2.0
date-released: Dec 8, 2025
authors:
  - family-names: Bolan
    given-names: Matthew
    orcid: https://orcid.org/0009-0004-7373-1311
  - family-names: Breitner
    given-names: Joachim
    orcid: https://orcid.org/0000-0003-3753-6821
  - family-names: Brox
    given-names: Jose
    orcid: https://orcid.org/0000-0001-9822-5838
  - family-names: Carlini
    given-names: Nicholas
  - family-names: Carneiro
    given-names: Mario
    orcid: https://orcid.org/0000-0002-0470-5249
  - family-names: van Doorn
    given-names: Floris
    orcid: https://orcid.org/0000-0003-2899-8565
  - family-names: Dvorak
    given-names: Martin
    orcid: https://orcid.org/0000-0001-5293-214X
  - family-names: Goens
    given-names: Andres
    orcid: https://orcid.org/0000-0002-0409-1363
  - family-names: Hill
    given-names: Aaron
    orcid: https://orcid.org/0009-0007-0827-1277
  - family-names: Husum
    given-names: Harald
    orcid: https://orcid.org/0009-0003-0634-7435
  - family-names: Ibarra Mejia
    given-names: Hernán
  - family-names: Kocsis
    given-names: Zoltan A.
  - family-names: Le Floch
    given-names: Bruno
    orcid: https://orcid.org/0000-0002-3965-9705
  - family-names: Livne Bar-on
    given-names: Amir
  - family-names: Luccioli
    given-names: Lorenzo
    orcid: https://orcid.org/0009-0009-2256-2833
  - family-names: McNeil
    given-names: Douglas
    orcid: https://orcid.org/0009-0006-4662-0469
  - family-names: Meiburg
    given-names: Alex
    orcid: https://orcid.org/0000-0002-4506-9146
  - family-names: Monticone
    given-names: Pietro
    orcid: https://orcid.org/0000-0002-2731-9623
  - family-names: Nielsen
    given-names: Pace
  - family-names: Osazuwa
    given-names: Emmanuel Osalotioman
    orcid: https://orcid.org/0009-0003-1415-8263
  - family-names: Paolini
    given-names: Giovanni
    orcid: https://orcid.org/0000-0002-3964-9101
  - family-names: Petracci
    given-names: Marco
  - family-names: Reinke
    given-names: Bernhard
    orcid: https://orcid.org/0000-0001-9024-2449
  - family-names: Renshaw
    given-names: David
    orcid: https://orcid.org/0000-0002-9987-9144
  - family-names: Rossel
    given-names: Marcus
    orcid: https://orcid.org/0009-0001-3567-6890
  - family-names: Roux
    given-names: Cody
    orcid: https://orcid.org/0009-0004-5304-037X
  - family-names: Scanvic
    given-names: Jérémy
    orcid: https://orcid.org/0009-0003-6117-0492
  - family-names: Srinivas
    given-names: Shreyas
    orcid: https://orcid.org/0000-0002-3993-1596
  - family-names: Tadipatri
    given-names: Anand Rao
    orcid: https://orcid.org/0009-0007-0057-4169
  - family-names: Tao
    given-names: Terence
    orcid: https://orcid.org/0000-0002-0140-7641
  - family-names: Tsyrklevich
    given-names: Vlad
    orcid: https://orcid.org/0009-0009-9511-5460
  - family-names: Vaquerizo-Villar
    given-names: Fernando
    orcid: https://orcid.org/0000-0002-5898-2006
  - family-names: Weber
    given-names: Daniel
    orcid: https://orcid.org/0009-0008-4615-6445
  - family-names: Zheng
    given-names: Fan
repository-code: https://github.com/teorth/equational_theories
url: https://github.com/teorth/equational_theories
abstract: >
  A collaborative project to determine the logical relations between 4694 equational laws of magmas, and formalize them in the Lean4 proof assistant language.  The project produced a research paper https://teorth.github.io/equational_theories/paper.pdf, as well as a "blueprint" https://teorth.github.io/equational_theories/blueprint/ containing a significant amount of supplemental information that

  Organized by Pietro Monticone, Shreyas Srinivas, and Terence Tao. Launched Sep 26, 2024.
keywords:
  - universal algebra
  - formalization project