The purpose of this project, launched on Sep 25, 2024, is to explore the space of equational theories of magmas, ordered by implication. To begin with we shall focus only on theories of a single equation, and specifically on this list of 4694 equations (all laws involving at most four magma operations, up to symmetry and relabeling). This creates 4694*(4694-1) = 22,028,942 implications that need to be proven or disproven.

Some selected equations are listed here. A (manually created) Hasse diagram of the dependencies obtained so far for these selected equations can be found here.

Some automatically generated progress:

• Sep 28, 2024: 85 laws have been shown to be equivalent to the constant law Equation46, and 815 laws have been shown to be equivalent to the singleton law Equation2.
• Sep 28, 2024: 18972 implications were established by simple rewrite laws.

Coming soon: statistics on how many implications have been established so far, and visualization tools to explore the implication graph.

For guidelines on how to contribute, see the CONTRIBUTING.md file.

Links:

• Main web page
  • Blueprint
  • Documentation
  • The Lean Zulip stream for the project
• A blog post describing the project., Sep 25, 2024.
• Initial discussion on Zulip, Sep 26, 2024.
• Initial discusson on Mastodon, Jul 18, 2023.
  • Followup discussion on Mastodon, Sep 25, 2024.
• The MathOverflow post that inspired the project, Jul 17, 2023.
  • A related MathOverflow post, Jul 16, 2023.
• Automated provers for equational theories
  • Prover9 and Mace4
    • aa - a project to use Prover9/Mace4 to brute force axioms for finite mathematical domains
  • Vampire
  • eprover
  • twee
  • zipperposition
  • Z3
  • Knuckledragger
  • A blog post by Philip Zucker testing many of the above provers on a sample implication of this project.
  • "Guided Equality Saturation", Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer, Jan 5, 2024.
  • "Rewrite Rule Inference Using Equality Saturation", Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock, 23 Aug, 2021.
• Other tools
  • egg - e-graphs good