The purpose of this project 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, which are listed here.

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

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