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.

A (manually created) graph of the dependencies obtained so far can be found here, current as of Sep 27 2024.

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
  • Vampire
  • eprover
  • twee
  • zipperposition
  • "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