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:

• dashboard

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

This is the beginning of the README. Read the rest at the original. Read the full README ↗