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
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
以上為 README 的開頭部分。其餘內容請閱讀原文。 檢視完整 README ↗
