Classify all 653 associative equational laws of order up to 4, together with all their conjunctions, up to equivalence, and determine every implication between the resulting theories.

Prover9/Mace4 automated theorem proving and model finding determine the implication graph. A minimal representative is selected for each equivalence class, using the Equational Theories Project's equation numbering. The implications and conjunction results are formalized in Lean, building on ETP tools such as the conversion from Vampire output to Lean code. Lean theorems state equivalence of each law to a theory, closure under conjunction, and soundness of an implication-checking function.

The 653 laws fall into 122 equivalence classes, and their conjunctions fall into 456 theories, forming a semilattice. The results are unchanged when restricting to finite semigroups. All implications and conjunctions are formalized in Lean, but there is no end-to-end theorem yet, and the completeness step (that the list of 653 equations covers all laws of order at most 4) is not formalized.