Dec 2025
Equational Theories Project
Model / AI: Classical automated provers
machine-checked
all 22,028,942 non-reflexive implications between the 4694 simplest magma laws determined and formalized in Lean, via explicit proofs and countermodels plus transitive closure, completing the primary goal on 14 April 2025; one case and its dual remain open in the separate finite-magma graph. Most of the work was done by classical automated theorem provers rather than LLMs, and Tao reports that "modern AI tools did not play a major role in this project". Paper.
Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.