equational-theories

Mathematics Distillation Challenge, Equational Theories. Stage 1 cheatsheet and Stage 2 Lean 4 certificate solver for the SAIR Foundation competition.

A single index to every SAIR Foundation challenge entered: the open problem each one states, the repository holding the method and the code, and what that method actually reached. Open science competitions in mathematics and computation, run by the Foundation for Science and AI Research.

Lean 4 formalization of the Spine Isolation Theorem for Magma Implications

Public companion to Lean-checked equational implication solvers: frozen artifacts, released-input evaluations, and an English research paper.

Lean 4: one-generated (1518+3862)-magmas are trivial or the Z/3 shift, and constant-coefficient magma cohomology cannot refute 1518 => 47, 614, 817, 3862 (ETP laws; constant coefficients only, no new implication)

Fast finite-counterexample search for implications between equational laws over magmas

How much of Le Floch's implication semilattice of Schröder's 990 quasigroup laws (arXiv:2603.29909) small quasigroups witness. Exhaustive Rust enumeration, exact results to order 9, independent checks, generated report and paper.

Mathematical exploration tool for finite Magmas and equational theories

Magma signature and coverage engine over the Equational Theories Project law set