Les agents IA d'Axiom formalisent la classification des groupes simples finis dans Lean

Axiom Math a déclaré le 26 octobre 2026 qu’elle avait publié la première preuve complète vérifiée par ordinateur de la Classification des groupes simples finis, écrite dans l’assistant de preuve Lean [1]. Sur 24 jours, ses ingénieurs et mathématiciens ont dirigé des essaims de dizaines d’agents IA qui ont produit environ 43,1 millions de lignes de code Lean [1][2].

Qu’a formalisé Axiom ?

La classification, souvent appelée l’énorme théorème, énumère les blocs de construction de tous les groupes finis, les mathématiques de la symétrie [1]. Elle affirme que tout groupe simple fini est cyclique d’ordre premier, alterné, de type de Lie ou l’un des 26 groupes sporadiques [2].

Axiom indique que la preuve originale s’étend sur environ 15 000 pages dans plus de 500 articles rédigés par une centaine de mathématiciens [1]. Sa version Lean suit la preuve de première génération et, selon la page GitHub du projet, est sans regret, c’est-à-dire qu’aucune étape n’est laissée non prouvée [3].

Axiom dit que ses agents IA ont produit environ 43,1 millions de lignes de Lean en 24 jours pour formaliser la classification. Le site du projet liste 2,05 millions de déclarations et 715 articles et livres dans le corpus [2]. Axiom indique que la formalisation incorpore environ 1,2 million de lignes d’un projet antérieur, Qiuzhen-CFSG, et s’appuie sur la bibliothèque Mathlib [1].

Comment fonctionnait l’essaim d’agents ?

Axiom a ouvert un canal Slack pour le projet le 1er octobre 2026 et le premier essaim est entré en service le 2 octobre [1]. Une carte de preuve tirée de la littérature a divisé le travail en 108 jalons et environ 380 tâches plus petites, que les agents ont revendiquées via des issues GitHub [1].

Les agents principaux ont décomposé les arguments difficiles et examiné les énoncés, tandis que d’autres ont recherché des résultats existants ou écrit des preuves Lean [1]. Des mathématiciens humains ont géré les obstructions mathématiques et des ingénieurs ont maintenu le système en marche [1]. Axiom indique qu’elle a supprimé des dizaines de milliers de lignes construites sur des hypothèses non prouvées et a redémarré des parties du travail [1].

Le 10 octobre, selon Axiom, un message dans le canal a annoncé que les agents avaient prouvé que le groupe Monstre est simple [1]. Lean vérifie les déductions, tandis que les humains inspectent l’énoncé final et les définitions pour confirmer qu’ils expriment le théorème visé [1].

Quelles erreurs les agents IA ont-ils trouvées ?

Axiom indique que la plupart des problèmes qu’elle a trouvés étaient mineurs, tels que des erreurs typographiques, des fautes dans les tableaux ou des hypothèses omises [1]. Axiom a trouvé 34 écarts notables par rapport au registre publié qui devaient être résolus. Le cas le plus substantiel concernait le théorème du groupe déséquilibré [1][2].

Là, les agents ont trouvé des contre-exemples à une assertion de clôture dans l’argument de John Walter de 1986, ce qui a laissé une étape clé non justifiée sans réfuter le théorème lui-même [1]. Un argument alternatif construit sur la théorie des 2-composantes maximales de Ronald Solomon de 1976 est devenu un nouveau résultat, rédigé dans un article de 35 pages [1][2]. Solomon et Richard Lyons, qui ont travaillé sur la classification originale, ont été consultés [1].

Quelqu’un en dehors d’Axiom a-t-il vérifié la preuve ?

Pas encore, selon RuntimeWire [4]. Carina Hong, PDG d’Axiom, a déclaré à RuntimeWire qu’aucun groupe extérieur n’a encore reconstruit et vérifié la preuve. Axiom publie les artefacts de build pour que d’autres puissent la reproduire [4].

La page GitHub indique qu’une seule commande de build vérifie l’ensemble du projet, et qu’Axiom a utilisé des modifications en attente de Lake, l’outil de build de Lean, pour ramener le temps de build sous 24 heures [3]. The AI Pin a couvert les affirmations distinctes d’OpenAI concernant de nouvelles découvertes mathématiques le 27 octobre.

Notre lecture

Opinion : Auditer une preuve qu’aucune personne seule n’a jamais lue entièrement est un usage plus convaincant de l’IA en mathématiques que la course aux gros titres, et trouver 34 écarts réels montre que l’audit avait du mordant. Le résultat n’est cependant aussi solide que ses vérifications externes, donc une reconstruction indépendante et un examen des errata en théorie des groupes comptent plus que le nombre de lignes.

Ce que nous n’avons pas pu vérifier

• Si la preuve de 43,1 millions de lignes se construit et se vérifie en dehors d’Axiom ; selon RuntimeWire, aucun groupe extérieur n’avait terminé une reconstruction au 27 octobre 2026.
• Quels modèles d’IA alimentaient les agents ; Axiom indique seulement qu’ils ont utilisé un mélange changeant de modèles.
• Comment les théoriciens des groupes indépendants jugent le résultat ; nous n’avons trouvé aucune réaction publiée d’un théoricien des groupes extérieur au cercle consultatif d’Axiom à la publication.
• La liste complète des 34 écarts notables ; Axiom indique qu’elle publiera la liste des errata après consultation des théoriciens des groupes.
• Si le nouvel article sur le théorème du groupe déséquilibré tient la route lors d’un examen par les pairs ; il est publié sur Hexagon, et nous n’avons pas pu confirmer de relecture par les pairs dans une revue.