Collaboration and Innovation in the Equational Theories Project: Formalizing Mathematics with Lean 4

This thesis explores the ``Equational Theories'' project, an innovative initiative launched by Terence Tao which combines collaboration between professional and amateur mathematicians with the use of artificial intelligence tools and proof-assistant languages, such as Lean 4. The project focuses on the study of equational theories in universal algebra, particularly on magmas (sets equipped with a binary operation), with the goal of determining the implications between different algebraic equations and constructing an implication graph. A central aspect of this thesis is the greedy construction, an iterative algorithm that enables the construction of infinite magmas satisfying specific equations. This method has been applied in detail to prove the non-implication 1516-255, through the construction of a counterexample. The formalization in Lean revealed errors in the informal version of the proof, highlighting the importance of formalization in ensuring the correctness of the results. This thesis also introduces magma cohomology, a new mathematical structure that emerged during the project, which generalizes group cohomology and has proven useful in resolving finite implications. In summary, the project represents an innovative approach to mathematical research, based on open collaboration, advanced computational tools, and rigorous formalization, paving the way for future explorations in this field.