Equational theories 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.
Here is a tour of several selected equations, including the ones above.
Current statistics and data files, updated automatically:
Current visualizations, updated automatically:
- Equation Explorer is a tool for exploring the graph of equation implications.
- Finite Magma Explorer is a tool for exploring finite magmas and the equations they satisfy.
- Graphiti is a tool for visualizing the implication graph.
For guidelines on how to contribute, see the CONTRIBUTING.md file. Participants are requested to abide by our code of conduct.
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
- A blog post describing the project., Sep 25, 2024.
- The equational theories project: a brief tour, Oct 12, 2024 - a followup to the previous post.
- 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. Larger list with equations of up to five operations
- List of duals of equations (JSON)
- The smallest magma obeying a given equation (up to N=5), if it exists (and the magmas themselves)
- To download the current state of the implication graph, see this thread.
- 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 inEquations/All.lean
find_dual
– finds the dual of an equationfind_equation_id
– finds the equation number of an equation stringfind_powerful_theorems.py
– finds theorems that, if proved, would imply many othersgenerate_eqs_list
– generates a list of equationsgenerate_image
– generates an image of implicationsgenerate_most_wanted_list
– generates the "most wanted" implicationsgenerate_z3_counterexample
– given an implication statement between two equations, calls Z3 to try to generate a counterexampleprocess_implications
– processes implications from one or more Lean files
- Ruby
generate_graphviz_graph
– creates a graphviz graphtransitive_closure
– computes the transitive closure of a set of implicationstransitive_reduction
– finds a transitive reduction of a set of implicationsgraph
– graph library
- Shell
- 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.
- Prover9 and Mace4
- Other tools
- egg - e-graphs good
- MiniZinc – high-level constraint modeling language
- nauty – graph automorphism tool
- KBCV – Knuth-Bendix completion visualizer
- Instagraph – knowledge graph generator
- Logic Programming in F# – Code and Examples from John Harrison's "Handbook of Practical Logic and Automated Reasoning"
- Blog posts and media mentioning this project
- "We're Entering Uncharted Territory for Math", Matteo Wong, The Atlantic, Oct 4 2024.
- "On Math Platform", Michael Bucko, Substack von Michael, Oct 5 2024.