Axiom Math, une entreprise d’intelligence artificielle basée à Palo Alto, affirme avoir réalisé en 24 jours la première formalisation entièrement vérifiée par ordinateur de la classification des groupes simples finis, un théorème monumental long d’environ 15 000 pages. Son système AxiomProver a converti l’argument en langage Lean, produisant environ 43,1 millions de lignes de code, soit la plus grande base de code Lean jamais créée. Le processus a permis de corriger plus de 2 000 erreurs dans la littérature existante, dont 34 écarts notables, et de combler une lacune importante dans le théorème des groupes non équilibrés. La formalisation confirme que les groupes simples finis se répartissent en quatre catégories et confirme que la liste est complète, tandis que le système multi-agents a été supervisé par des mathématiciens experts.
Source: Lire l’article original
