Axiom Math publie une preuve Lean de la classification des groupes, longue de 43,1 millions de lignes

Le 27 octobre 2026, Axiom Math a annoncé la publication de ce qu’elle présente comme la première preuve complète, vérifiée par ordinateur, de la classification des groupes simples finis. Réalisée en 24 jours, elle est le fruit du travail d’ingénieurs et de mathématiciens qui ont dirigé des essaims de dizaines d’agents d’IA, lesquels ont écrit environ 43,1 millions de lignes de code dans l’assistant de preuve Lean.

« Aujourd’hui, nous publions la première preuve complète, vérifiée par ordinateur, de la classification des groupes simples finis (CFSG) », a écrit l’entreprise dans son annonce. Cette classification définit les éléments constitutifs fondamentaux des groupes finis. Sa preuve originale s’étend sur environ 15 000 pages réparties dans plus de 500 articles signés par quelque 100 mathématiciens, une ampleur qui lui a valu le surnom de « théorème gigantesque ».

Ce qu’Axiom a publié

La CFSG établit que tout groupe simple fini est soit cyclique d’ordre premier, soit alterné sur au moins cinq lettres, soit membre de l’une des seize familles infinies de groupes de type Lie construites sur des corps finis, soit l’un des 26 groupes sporadiques isolés — exactement 26. L’annonce précise que certains auteurs comptent le groupe de Tits comme un 27e groupe. Le plus grand groupe sporadique, le Monstre, a été construit par Robert Griess en 1980 à l’aide d’une algèbre de dimension 196 884.

La démonstration menée par des mathématiciens s’est étalée sur plusieurs décennies. En 1963, Walter Feit et John Thompson ont démontré que tout groupe simple fini non abélien est d’ordre pair, dans un article de 255 pages qui remplissait un numéro entier du Pacific Journal of Mathematics. En 1972, Daniel Gorenstein a présenté un programme en seize étapes pour achever la classification, qu’il a déclarée complète en 1983. Toutefois, le cas quasiminuscule reposait sur un manuscrit inachevé de Geoffrey Mason, jusqu’à ce que Michael Aschbacher et Stephen Smith publient en 2004 une étude de 1 221 pages, mettant ainsi un terme à ce qui allait être appelé la preuve de première génération. Une preuve de deuxième génération, plus systématique, entreprise par Gorenstein et Richard Lyons, puis rejointe par Ronald Solomon et Inna Capdeboscq, reste inachevée. Axiom a donc formalisé la preuve de première génération.

La page du projet indique que la formalisation suit la preuve de première génération et que chaque étape logique est vérifiée par le noyau de Lean. Elle recense 43,1 millions de lignes de Lean, 2,05 millions de déclarations et 715 articles et ouvrages dans son corpus. Axiom explique que sa carte de la preuve s’appuie sur les volumes de la preuve de deuxième génération et que la formalisation intègre environ 1,2 million de lignes de code issues du projet antérieur Qiuzhen-CFSG. Elle s’appuie également sur Mathlib, auquel l’entreprise attribue le mérite de centaines de contributeurs. Le projet cite Dean Cureton, Vasily Ilin, Bhavik Mehta et Niels Voss comme contributeurs principaux, et Letong Hong comme chercheur principal.

Dépôt public sur GitHub, le projet présente le résultat comme une preuve Lean4 sans recours à sorry, épinglée à la version 4.35.0-rc3, fondée sur Mathlib et le projet TauCeti et n’utilisant que les axiomes standards Classical.choice, propext et Quot.sound, sans native_decide. L’énoncé formel de la classification, repris de TauCeti, est le suivant : « Tout groupe simple fini est isomorphe à l’un des groupes explicitement construits dans la liste de classification. » Le fichier README indique que lake build vérifie l’ensemble du développement et que des modifications en cours de l’outil de compilation Lake, ainsi que des optimisations que l’équipe prévoit de proposer en amont, ont ramené le temps de compilation à moins de 24 heures. Le code est distribué sous licence Apache-2.0.

Un travail mené par un essaim en 24 jours

Le 1er octobre 2026, Axiom a ouvert un canal Slack pour coordonner le projet. Les travaux déjà réalisés sur Lean et une carte interne de la preuve, élaborée à partir de la littérature publiée, ont réparti le travail en 108 jalons et environ 380 tâches plus petites. Le premier essaim a été lancé le 2 octobre 2026 : les agents se sont attribué des jalons par l’intermédiaire de tickets GitHub et ont rendu compte de leur travail terminé sur Slack. Les agents principaux décomposaient les arguments difficiles et examinaient les énoncés, tandis que d’autres recherchaient des résultats existants ou rédigeaient des preuves Lean. Un agent pouvait aussi déléguer à d’autres agents la recherche de prérequis manquants, dont les résultats étaient ensuite intégrés à un dépôt partagé.

Les premiers progrès ont mis au jour des points faibles. Certains jalons qui semblaient réalisables dissimulaient d’énormes prérequis que les agents avaient présumés au lieu de les démontrer. L’équipe a donc supprimé des dizaines de milliers de lignes fondées sur ces hypothèses avant de reprendre le travail sur des bases plus solides. L’un des premiers jalons portait sur le théorème du foncteur signaliseur, dont la preuve candidate reposait sur des hypothèses structurelles qui restaient à justifier. Le temps de compilation est également devenu un goulot d’étranglement, les agents produisant des preuves plus vite que Lean ne pouvait les vérifier à nouveau. Axiom indique que ses ingénieurs ont réparti les résultats de compilation mis en cache entre les machines de travail, lancé des vérifications indépendantes en parallèle et déporté les calculs finis coûteux dans des certificats vérifiables séparément. Selon l’entreprise, ces changements ont accéléré la vérification de plusieurs ordres de grandeur.

Le 10 octobre 2026, un message publié sur le canal a annoncé que les agents avaient démontré la simplicité du Monstre, rapporte l’entreprise. Les agents ont également formalisé l’existence du Monstre au moyen de l’algèbre de Griess, ainsi qu’un théorème identifiant les groupes de type Monstre au Monstre. Le 13 octobre 2026, un seul jalon a été achevé. Les ingénieurs ont alors organisé une nouvelle planification et divisé les jalons inachevés en théorèmes plus petits, formulés avec précision. Pour chaque décomposition, il fallait montrer au moyen d’une courte preuve Lean comment les différentes parties permettraient d’établir le jalon d’origine.

Des lacunes relevées dans la preuve publiée

La traduction de la démonstration en Lean a mis au jour des problèmes dans les arguments publiés, rapporte Axiom. La plupart étaient mineurs — erreurs typographiques, erreurs dans des tableaux ou hypothèses omises —, mais l’entreprise dénombre 34 écarts notables par rapport à la publication, dont le plus important concerne l’Unbalanced Group Theorem, ou UGT.

Un exemple se trouvait dans les volumes d’Aschbacher et Smith consacrés aux groupes quasi-minces : un lemme y affirmait que deux quantités numériques étaient égales. Les agents ont trouvé un contre-exemple faisant intervenir le groupe SL₂(5), dans lequel l’une des quantités valait 1 alors que l’égalité affirmée exigeait qu’elle vaille 2. Remplacer l’égalité par une inégalité a corrigé le lemme, mais des arguments ultérieurs s’appuyaient sur l’égalité pour exclure certains cas ; l’équipe a donc élargi un argument antérieur afin de couvrir ces configurations.

L’UGT permet d’identifier un groupe entier à partir d’informations sur ses sous-groupes : selon le résumé de l’article qui l’accompagne, sous les hypothèses inductives de la classification, la présence d’un sous-groupe non trivial d’ordre impair, normal dans le centralisateur d’une involution, implique que le groupe simple ambiant est de type Lie en caractéristique impaire ou alterné de certains degrés. Axiom a abordé l’UGT à partir des mémoires de John Walter publiés en 1986 et, en formalisant cet argument, ses agents ont trouvé des contre-exemples explicites à une propriété de stabilité utilisée dans celui-ci : une opération supposée maintenir les groupes simples associés dans une famille donnée pouvait produire un groupe explicitement exclu de cette famille.

Selon l’explication de l’entreprise, en partant de PSL₂(49), dont l’involution de corps a pour centralisateur PGL₂(7), l’opération donne la composante simple PSL₂(7), exclue de la famille parce que 7 est un nombre premier de Mersenne. Axiom précise que les contre-exemples ne réfutaient ni l’UGT elle-même ni même la conclusion de la proposition II.5.9(ii) de Walter.

La correction s’appuie sur la théorie des 2-composantes maximales de Solomon, datant de 1976, qui, selon Axiom, a fourni les idées essentielles d’un argument de remplacement élaboré et formalisé par son système AxiomProver. L’étape clé, énoncée dans l’article sous le nom de théorème 2.3 (préservation des sommets simples), est présentée par Axiom comme un résultat inédit en théorie des groupes, démontré par AxiomProver ; combinée aux réductions de Gilman et Solomon et aux théorèmes de reconnaissance de Foote et Harris, elle fournit la forme en groupes simples de l’UGT nécessaire à la classification. Après la formalisation, les mathématiciens d’Axiom ont trouvé une déduction plus courte, fondée sur des méthodes de première génération et consignée dans la remarque 9.5, qui aboutit à la même conclusion sans recourir au théorème 2.3.

Cet article, The Unbalanced Group Theorem, auquel ont contribué Colin Defant et Ken Ono, a été publié sur le serveur de prépublications Hexagon dans sa version 1 le 27 octobre 2026, sous licence CC BY 4.0 ; la page du projet indique qu’il compte 35 pages. Axiom affirme travailler avec des spécialistes de la théorie des groupes pour compiler les errata relevés dans la littérature et les publier sur la page des errata du projet. Lyons et Solomon, dont les travaux sous-tendent la classification, ont été consultés au sujet de la correction de l’UGT, et l’entreprise indique qu’elle continuera à recenser les errata et à y remédier avec l’aide d’un comité consultatif qui les inclut, ainsi que du conseiller externe Dan Nakano. Axiom présente sa contribution comme le fait de rendre la démonstration vérifiable mécaniquement, de documenter les obstacles rencontrés et de fournir des arguments formalisés pour les résoudre, tout en précisant que la classification reste l’œuvre des mathématiciens qui ont découvert les groupes et élaboré les arguments.