Reservoir

Equational theory project

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 the 4694 equational laws involving at most four magma operations, up to symmetry and relabeling (here is the list in Lean and in plain text). This creates 4694*(4694-1) = 22,028,942 implications that need to be proven or disproven, creating both "implications" and "anti-implications".

We will accumulate both "proven" and "conjectured" implications and anti-implications: proven assertions will be verified in the proof assistant language Lean, and "conjectured" assertions represent all claims (either human-generated or computer-generated) that have not yet been verified in Lean. The current status of the project can be found on the dashboard.

Some selected equations of interest are listed here (in Lean form) and here (in a human readable blueprint). Examples include

• Equation 1: x = x. The trivial law.
• Equation 2: x = y. The singleton law.
• Equation 43: x ◇ y = y ◇ x. The commutative law.
• Equation 46: x ◇ y = z ◇ w. The constant law.
• Equation 4512: x ◇ (y ◇ z) = (x ◇ y) ◇ z. The associative law.

(Note: in some legacy portions of this project, the magma operation was denoted ◦︎ instead of ◇.) Here is a tour of several selected equations, including the ones above.

Current statistics and data files, updated automatically:

• dashboard

Current visualizations, updated automatically:

• A tool for exploring the graph of equation implications is available here.
• An experimental tool to interactively explore a Hasse diagram of the graph is available here

For guidelines on how to contribute, see the CONTRIBUTING.md file. Participants are requested to abide by our code of conduct.

Past progress

Some automatically generated progress:

• Sep 28, 2024: 85 laws have been shown to be equivalent to the constant law (Equation 46), and 815 laws have been shown to be equivalent to the singleton law (Equation2). Discussed in the blueprint here.
• Sep 28, 2024: 18972 implications were established by simple rewrite laws. Discussed in the blueprint here.
• Sep 28, 2024: 4.2m implications proven by a transitive reduction of 15k theorems were proven using simple rewrite proof scripts. Discussed in the blueprint here.
• Sep 29, 2024: 13.7m implications were conjectured to be refuted by a collection of 515 magmas, collected by enumerating all 4^(4*4) operators and reducing to a covering set. Discussed in the blueprint here. (Update, Oct 3, 2024: these anti-implications are now formalized in Lean as theorems, and the number of implications established by this method increased to 13.8m.)
• Oct 1, 2024: Another ~250k transitive implications were proven by simple proof generation. Discussed in the blueprint here.
• Oct 1, 2024: ~500k transitive implications were proven by EquationSearch, a custom tool that chooses hypotheses and leverages previously found implications to search by using the implied equations as substitutions. Discussed in the blueprint here.
• Oct 2, 2024: 86 (potentially) new implications in Subgraph.lean conclusively (i.e. in Lean) resolved using the lean-egg tactic. Some of these were simply missed by the transitive closure computation and technically already implied, but some were genuinely new.
• Oct 3, 2024: Another ~150k transitive implications were proven by EquationSearch after improved capabilities were added.
• Oct 3, 2024: ~1m transitive implications were proven by a new custom tool that uses egraphs to find a proof and exports it to a Lean term
• Oct 5, 2024: 97% of the remaining unknown implications were resolved (transitively) by Vampire, and then converted to a Lean proof using a custom script and a Lean elaborator implementing the deduction step of superposition calculus.

Some statistics and data files from a given point in time:

• Sep 28, 2024: A repository of unknown implications, including all unknown implications, known equivalence classes, unknown implications modulo known equivalence, and only the strongest unknown implications.
• Sep 29, 2024: Here is a text file of the (21K or so) direct implications proven to date, and here is the transitive closure of these implications (about 4.5m). More precisely, we have 21791 implications explicitly proven true, 4494090 additional relations implicitly proven true, 739207 explicitly proven false, 12764328 implicitly proven false, one additional relations explicitly conjectured true (and 64 more implicitly conjectured true), and 4014155 remaining implications which remain completely open. Quotienting out by known equivalences, there are 3182453 open implications remaining.
• Oct 2, 2024: A list of unknown implications whose converse is proven, i.e. implications that would reduce the number of equivalence classes of equations. At the time of creation we had 2969 equivalence classes. This file contains 4526 unknown implications, if all hold then it will reduce the number of equivalence classes to 1300.
• Oct 4, 2024: Current dashboard status: 29248 explicitly proven, 7063191 implicitly proven, 605854 explicitly disproven, 13243426 implicitly disproven, 1120090 open (94.923% complete). No conjectures at this time. (A more formal time series of progress is planned.)
• Oct 5, 2024: Current dashboard status: 31023 explicitly proven, 8151818 implicitly proven, 581166 explicitly disproven, 13268299 implicitly proven, 29503 open (99.866% complete). Note some pruning of redundant theorems occurred in the explicitly disproven theorems to improve compilation time.

Some visualizations from a given point in time:

• Sep 28, 2024: A (manually created) Hasse diagram of the dependencies obtained up to this date for the selected equations of interest can be found here. Note: the orientation in these legacy images is reversed from that in current guidance.
• Sep 28, 2024: A directed acyclic graph of automatically generated implications is here: circular vertices are for nodes representing multiple equivalent equations and equations in green are from Subgraph.lean. Note: the orientation in these legacy images is reversed from that in current guidance.
• Oct 1, 2024: An image visualizing the graph of proved results can be found here. This was generated by outcomes_to_image.py.
• Oct 3, 2024: The current implications represented as a directed acyclic graph were generated using generate_graphviz_graph.rb to visualize the entire graph and the smaller graph of equations limited to 3 variables and three operations. As previously: circular vertices are for nodes representing multiple equivalent equations and vertices in green are from Subgraph.lean.

Building the project

To build this project after installing Lean and cloning this repository, follow these steps:

% cd equational_theories/
% lake exe cache get
% lake build

Links

• Main web page
  • Blueprint
  • Documentation
  • The Lean Zulip stream for the project
  • Instructions on how to contribute
  • Code of conduct
• A blog post describing the project., Sep 25, 2024.
• Initial discussion on Zulip, Sep 26, 2024.
• Initial discussion 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.
• Data
  • Text list of equations
  • List of duals of equations
  • The smallest magma obeying a given equation (up to N=5), if it exists
• Scripts
  • Shell
    • run_before_push - performs some of the CI checks, suitable for running just before pushing a new PR
  • Lean
    • extract_implications - extracts implications from one or more Lean files. This outputs the "ground truth" of implication data, for use by other scripts
  • Python
    • explore_magma - test a given magma table against all or a subset of the equations in AllEquations.lean
    • find_dual - finds the dual of an equation
    • find_equation_id - finds the equation number of an equation string
    • find_powerful_theorems.py - finds theorems that, if proved, would imply many others
    • generate_eqs_list - generates a list of equations
    • generate_graphviz_graph - generates a graphviz dot file, that can be used to create an implication graph
    • generate_image - generates an image of implications
    • generate_most_wanted_list - generates the "most wanted" implications
    • generate_z3_counterexample - given an implication statement between two equations, calls Z3 to try to generate a counterexample
    • process_implications - processes implications from one or more Lean files
  • Ruby
    • generate_graphviz_graph - creates a graphviz graph
    • graph - graph condensation tools
    • transitive_closure - computes the transitive closure of a set of implications
    • transitive_reduction - finds a transitive reduction of a set of implications
• 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