Il y a presque trois semaines, j'ai proposé un projet collaboratif, combinant les efforts de mathématiciens professionnels et amateurs, de démonstrateurs de théorèmes automatiques, d'outils d'intelligence artificielle et du langage d'assistant de preuve Lean, pour décrire le graphe d'implication reliant les 4694 lois équationnelles pour les magma qui peuvent être exprimées en utilisant jusqu'à quatre invocations de l'opération magma. C'est-à-dire […]