Le 26 octobre 2026, Axiom Math a publié ce qu’elle présente comme la première preuve complète, vérifiée par ordinateur, de la classification des groupes simples finis, le théorème qui recense toutes les briques de base de la symétrie finie. D’après Axiom, la preuve d’origine passe généralement pour la plus longue jamais écrite par des humains : environ 15 000 pages, dans plus de 500 articles signés par une centaine de mathématiciens. Selon l’entreprise, ses ingénieurs et ses mathématiciens ont dirigé pendant 24 jours des essaims de plusieurs dizaines d’agents IA et abouti à environ 43,1 millions de lignes en Lean, un assistant de preuve dont le noyau contrôle chaque étape logique.
Formaliser la première grande étape de cette preuve, le théorème de Feit-Thompson et ses 255 pages, avait pris plus de six ans à l’équipe de Georges Gonthier au centre commun Microsoft Research-Inria, jusqu’en septembre 2012. Le code d’Axiom, publié sur GitHub le 27 octobre, s’appuie sur Mathlib, la bibliothèque mathématique de Lean, et reprend environ 1,2 million de lignes de Qiuzhen-CFSG, un projet qui avait déjà formalisé Feit-Thompson avec l’aide de l’IA. Aucune équipe extérieure à Axiom n’a encore reconstruit la preuve, a indiqué sa PDG le même jour.
Un tableau périodique de la symétrie
En mathématiques, un groupe rassemble les façons de transformer un objet sans changer son apparence. Axiom prend l’exemple d’un cube : 24 rotations le laissent exactement tel qu’il était. Tout groupe fini se décompose en morceaux insécables, les groupes simples finis, qu’Axiom appelle les atomes des groupes finis.
La classification en dresse la liste : les groupes cycliques d’ordre premier, les groupes alternés de degré au moins 5, 16 familles infinies dites de type de Lie et 26 groupes « sporadiques » isolés. Le plus grand d’entre eux, le Monstre, compte environ 8 × 10⁵³ éléments.
Daniel Gorenstein a annoncé en 1983 que la classification était achevée, avant de la surnommer « le théorème énorme ». L’annonce était prématurée : une lacune dans le cas dit « quasithin » est restée ouverte jusqu’au traitement de 1 221 pages publié en 2004 par Michael Aschbacher et Stephen Smith. « La plupart des gens qui comprenaient vraiment la preuve sont à la retraite ou ne sont plus parmi nous », a écrit sur X Vasily Ilin, d’Axiom, le 27 octobre.
Vingt-quatre jours et 108 jalons
Axiom a ouvert un canal Slack pour le projet le 1er octobre. Une carte de la preuve tirée des publications découpait le travail en 108 jalons et environ 380 tâches plus petites. Le 2 octobre, le premier essaim d’agents a démarré.
Les agents réservaient des jalons via des tickets GitHub, des agents principaux découpaient les arguments difficiles et relisaient les énoncés, d’autres écrivaient les preuves en Lean. Les mathématiciens de l’équipe traitaient les blocages mathématiques, les ingénieurs faisaient tourner le système.
Le plan initial a vite montré ses failles. Certains jalons cachaient de lourds prérequis que les agents avaient « supposés plutôt que démontrés », et l’équipe a supprimé des dizaines de milliers de lignes bâties sur ces hypothèses. Le 10 octobre, un message est tombé dans le canal : « WE PROVED MONSTER IS SIMPLE » (nous avons prouvé que le Monstre est simple). Le 13 octobre, un seul jalon a été bouclé, et les ingénieurs ont fait redécouper par des agents les jalons restants en théorèmes plus petits, énoncés avec précision.
La vérification est devenue le goulot d’étranglement. Selon Axiom, les agents produisaient des preuves plus vite que Lean ne pouvait les revérifier. Les ingénieurs ont partagé entre les machines les résultats de compilation mis en cache et déporté les calculs finis coûteux dans des certificats vérifiés à part, ce qui a accéléré la vérification « de plusieurs ordres de grandeur ».
34 écarts notables
L’essentiel des signalements des agents était mineur : coquilles, erreurs dans des tableaux, hypothèses oubliées. Axiom compte « 34 écarts notables par rapport aux publications » et prévoit de publier une liste d’errata avec des théoriciens des groupes. Sur X, Ilin donne un décompte plus large : « Nous avons trouvé des centaines d’erreurs dans la littérature existante, et écrit un article sur la plus importante, mais dans l’ensemble la preuve était juste. »
Dans les volumes d’Aschbacher et Smith sur les groupes quasithin, un lemme affirmait l’égalité de deux quantités. Les agents ont trouvé un contre-exemple dans le groupe SL₂(5), où l’une vaut 1 alors que l’égalité exigeait 2. L’équipe a remplacé l’égalité par une inégalité et repris les cas qui en dépendaient.
Le problème le plus sérieux touche au théorème des groupes non équilibrés (Unbalanced Group Theorem, UGT), qui règle un cas substantiel de la classification. En reprenant le mémoire de John Walter paru en 1986, les agents ont trouvé des contre-exemples explicites à une « assertion de clôture » de son raisonnement, dont l’un part du groupe PSL₂(49). Selon Axiom, la faille laissait « une inférence clé non justifiée », sans réfuter le théorème.
L’article d’accompagnement, mis en ligne le 27 octobre sous licence CC BY 4.0, précise que « l’UGT a aussi d’autres preuves ». Le 28 octobre, John D. Cook résumait sur son blog : « L’UGT, et la classification qui en dépend, sont justes, mais la preuve était fautive. »
La réparation s’appuie sur la théorie des 2-composantes maximales de Ronald Solomon (1976), et Axiom a consulté Solomon et Richard Lyons, deux des théoriciens des groupes à l’origine de la classification. D’après Axiom, son outil AxiomProver a produit et formalisé le nouvel argument, dont l’étape clé, le théorème 2.3 (« Preservation of simple tops »), est « un nouveau résultat en théorie des groupes ». L’article porte la mention « principalement écrit par des humains ». Après la formalisation, les mathématiciens d’Axiom ont trouvé vers l’UGT un chemin plus court, qui se passe du théorème 2.3.
Les précédents
La formalisation de Feit-Thompson achevée en 2012 comptait 170 000 lignes, selon Microsoft Research. Le 9 octobre, sur le blog de Terence Tao, Thomas Hales chiffrait la preuve formelle de la conjecture de Kepler à environ 20 années de travail humain et 500 000 lignes. Il y rappelait que l’autoformalisation du dernier théorème de Fermat, annoncée par Anthropic le 4 septembre, avait produit 13 millions de lignes de Lean en 11 jours.
Qiuzhen-CFSG, dont Axiom reprend le code, a décrit son travail le 11 août dans FormaTheoria, une prépublication cosignée notamment par Shing-Tung Yau : un développement Lean vérifié par machine, construit avec l’aide de l’IA, qui va jusqu’au théorème de Bender-Suzuki et couvre Feit-Thompson. En octobre, trois équipes ont déposé des preuves assistées par l’IA d’une conjecture de géométrie vieille de 31 ans, et Claude a écrit en quelques semaines des preuves vérifiées d’absence de plantage pour 123 bibliothèques open source. Le 26 octobre, jour du billet d’Axiom, OpenAI a affirmé avoir réfuté l’hypothèse du temps exponentiel, avec une version Lean qui, selon l’entreprise, était prête au lendemain de la découverte de l’argument par son modèle.
Les vérifications encore à faire
Les chiffres de la formalisation elle-même, des 24 jours aux 34 écarts, viennent d’Axiom. Dans un article de RuntimeWire publié le 27 octobre, sa PDG Carina Hong répond à la question de savoir si quelqu’un hors de l’entreprise a compilé et vérifié la preuve : « Pas encore. Nous publions les artefacts de compilation pour aider et encourager des tiers à la reproduire de façon indépendante. » Le dépôt précise que la compilation ne tient en moins de 24 heures qu’avec « quelques modifications en cours de Lake », l’outil de compilation de Lean, qu’Axiom compte faire intégrer à la version officielle.
Le noyau valide les déductions. La fidélité de l’énoncé formel à ce que les mathématiciens entendent relève d’un autre contrôle. Hales écrit qu’une preuve Lean « ne devrait jamais être crue avant d’avoir été vérifiée par le noyau », ni acceptée avant « un audit humain » de la fidélité de l’énoncé, une tâche « en général beaucoup plus facile que de vérifier la preuve elle-même ».
Axiom emprunte l’énoncé de la classification à un projet distinct, TauCeti, et indique que des humains l’examinent. Sa liste d’errata n’est pas encore en ligne, et l’article sur l’UGT est une prépublication.
Notre analyse
Les théoriciens des groupes ont démontré la classification il y a des décennies, et la version Lean d’Axiom aboutit au même théorème. Le gain de temps porte sur la vérification. La confiance dans le théorème repose sur plus de 500 articles et sur un cercle de plus en plus restreint d’experts capables de dire comment ils s’emboîtent. Axiom a rassemblé ce corpus dans un seul projet Lean que d’autres peuvent recompiler, avec un argument de remplacement pour la démonstration publiée de l’UGT et une liste d’errata promise.
Pour la classification entière, il reste surtout une reconstruction par des tiers et la relecture attentive d’un énoncé formel et des définitions qu’il utilise. Hales juge ce type d’audit beaucoup plus facile que la vérification d’une preuve. Axiom annonce une compilation en moins d’une journée, avec ses propres outils.
Hales note aussi que la formalisation de Navier-Stokes annoncée en septembre a déjà été confirmée par plus d’une douzaine de vérificateurs de preuves. Les prochains jalons pour la classification sont du même ordre : une reconstruction hors d’Axiom, la publication de la liste d’errata et l’avis des théoriciens des groupes sur le théorème 2.3, une fois l’article lu.
Sources
- Formalizing the Enormous Theorem, Axiom Math, 26 octobre 2026
- AxiomMath/CFSG: A Lean formalization of the Classification of Finite Simple Groups, Axiom Math, GitHub, 27 octobre 2026
- The Unbalanced Group Theorem, Axiom Math, déposé par Colin Defant et Ken Ono, Hexagon 2610.00575, 27 octobre 2026
- Message sur X, Vasily Ilin (Axiom Math), 27 octobre 2026
- Theorem Proof Gains Acclaim, Rob Knies, Microsoft Research, 11 octobre 2012
- FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature, Tianjiao Nie et al., arXiv, 11 août 2026
- Axiom publishes Lean proof artifacts to support independent reproduction, Emerson Redding, RuntimeWire, 27 octobre 2026
- What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI, Thomas Hales, billet invité sur le blog de Terence Tao, 9 octobre 2026
Image d’en-tête : graphique MACCUS, données d’Axiom Math (26 octobre 2026) et de Microsoft Research (11 octobre 2012)
