Axiom Math affirme que des agents d'IA ont formalisé en Lean la classification des groupes simples finis

Axiom Math, une start-up américaine qui développe des systèmes d'IA pour les mathématiques, a annoncé le 26 octobre 2026 avoir obtenu une preuve complète vérifiée par machine de la classification des groupes simples finis, l'un des résultats les plus longs des mathématiques. Le travail a été réalisé en Lean, un assistant de preuve dont le noyau contrôle chaque étape logique.

Ce qu'Axiom dit avoir accompli

La classification établit que tout groupe simple fini est soit cyclique d'ordre premier, soit alterné, soit un groupe de type de Lie, soit l'un des 26 groupes sporadiques. Sa preuve originale, achevée par de nombreux auteurs au fil des décennies, s'étend sur des milliers de pages de revues. Axiom a formalisé cette preuve de première génération ; une preuve de deuxième génération, publiée sous forme d'une série de volumes, reste inachevée.

D'après le billet de blog de l'entreprise, des dizaines d'agents tournant sur son système AxiomProver ont fourni l'essentiel de l'écriture en 24 jours. Des agents principaux découpaient les raisonnements et contrôlaient les énoncés, tandis que d'autres cherchaient des résultats existants ou rédigeaient les preuves en Lean, avec une combinaison changeante de modèles. Ingénieurs et mathématiciens pilotaient l'ensemble, étudiaient les obstacles mathématiques et traitaient les problèmes les plus lourds de conséquences. Selon Unite.AI, le premier essaim a démarré le 2 octobre. La page du projet fait état d'environ 43,1 millions de lignes de Lean et de 2,05 millions de déclarations, le code étant publié sur GitHub.

Des erreurs dans la littérature publiée

Axiom recense 34 écarts notables avec la littérature, pour la plupart mineurs : coquilles, erreurs dans des tables ou hypothèses omises. Le plus important concerne la démonstration du théorème des groupes non équilibrés (Unbalanced Group Theorem) par John Walter, où les agents ont trouvé des contre-exemples à une affirmation sur laquelle reposait l'argument. Axiom dit avoir comblé la lacune grâce à un nouveau résultat, après avoir consulté les spécialistes Richard Lyons et Ronald Solomon. L'entreprise signale aussi une égalité fausse dans un lemme des volumes d'Aschbacher et Smith sur les groupes « quasithin ». Selon elle, rien de cela ne remet en cause le théorème lui-même, et la liste complète des errata est publiée.

Précautions

Tous les chiffres proviennent des documents d'Axiom, et la page de statistiques du projet n'est pas entièrement cohérente : elle donne par exemple des nombres différents de jalons et d'ouvrages sources selon les endroits. Aucune évaluation indépendante n'est encore citée. Comme le rappelle l'entreprise, Lean vérifie les déductions, mais il revient aux humains de contrôler que l'énoncé formel et les définitions correspondent fidèlement aux mathématiques. Axiom, cofondée par Carina Hong et Shubho Sengupta, a levé 64 millions de dollars en 2025.