FAIRsharing record for: Equational Theories Project

This FAIRsharing record describes: 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. 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.