Equational theories project

License: Apache 2.0 Code Style: Black Website Documentation Blueprint Progress Paper Zulip Channel

Hasse diagram of selected equations

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

Here is a tour of several selected equations, including the ones above.

Current statistics and data files, updated automatically:

Current visualizations, updated automatically:

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