Equational theories database
dataset website , code repository
This database contains the complete set of implications between the 4694 equational laws for magmas involving at most four operations. These implications are formally verified in the proof assistant language Lean.