Axiom Math, une jeune pousse qui conçoit des systèmes d'IA pour les mathématiques, assure avoir converti l'une des plus longues démonstrations jamais écrites en code vérifiable étape par étape par une machine. Dans un billet daté du 26 octobre et un dépôt GitHub public annoncé le 27, l'entreprise a dévoilé une formalisation en Lean 4 de la classification des groupes simples finis (CFSG), surnommée le théorème énorme, en attribuant l'essentiel du travail à des essaims de ses agents AxiomProver encadrés par des ingénieurs et des mathématiciens.
Selon ce théorème, tout groupe simple fini est cyclique d'ordre premier, alterné, issu de l'une des familles de type de Lie, ou bien l'un des 26 groupes sporadiques, dont le plus grand est le Monstre. Ces groupes sont les briques élémentaires de tous les groupes finis. La preuve humaine s'étale sur quelque 15 000 pages réparties dans plus de 500 articles signés par une centaine d'auteurs ; annoncée comme achevée en 1983, elle n'a été bouclée qu'en 2004 grâce à un traitement de 1 221 pages du cas dit quasithin.
D'après Axiom, le chantier a duré 24 jours. Un canal de coordination a été ouvert le 1er octobre, puis une carte de la preuve tirée de la littérature, découpée en 108 jalons et environ 380 tâches, a permis aux agents de réserver du travail, de déléguer les prérequis manquants et de verser leurs résultats dans un dépôt commun. Des agents chefs décomposaient les arguments difficiles et contrôlaient les énoncés, tandis que d'autres cherchaient des résultats existants et rédigeaient le Lean. Le tout atteint environ 43,1 millions de lignes et, selon le site du projet, 2,05 millions de déclarations. Axiom ne précise pas quels modèles d'IA ont été employés.
Le README indique que le développement ne contient aucun sorry, cible Lean v4.35.0-rc3, s'appuie sur Mathlib et sur le projet TauCeti, dont il reprend l'énoncé de la classification, et n'utilise que les axiomes standard, sans native_decide. Il réutilise aussi environ 1,2 million de lignes du projet Qiuzhen-CFSG. Une compilation complète a demandé près d'une journée à Axiom, malgré des modifications encore non publiées de l'outil Lake. Le code est sous licence Apache 2.0.
Le plus intéressant tient peut-être à ce que les agents ont débusqué en chemin. Axiom recense 34 écarts notables par rapport aux textes publiés, surtout des erreurs mineures, mais aussi des contre-exemples à une étape de clôture dans la démonstration de l'Unbalanced Group Theorem proposée par John Walter en 1986. L'entreprise insiste : le théorème lui-même n'est pas remis en cause. Pour combler la lacune, AxiomProver a prouvé un nouveau résultat de préservation fondé sur la théorie des 2-composantes maximales de Ronald Solomon (1976), exposé dans un article dédié ; des mathématiciens d'Axiom ont ensuite trouvé un raisonnement plus court. Les spécialistes Richard Lyons et Ronald Solomon ont conseillé le projet et participeront à l'établissement d'une liste d'errata, qui n'a pas encore été publiée.
À titre de comparaison, le théorème de Feit-Thompson, long de 255 pages et simple pièce de la classification, avait demandé six ans à une équipe dirigée par Georges Gonthier pour être formalisé en Coq, travail achevé en 2012. Axiom présente son projet comme le prolongement de cette tradition et de Mathlib, et non comme un substitut aux mathématiciens auteurs de la preuve originale.
Les observateurs indépendants invitent à la prudence. Neural Brew, dans un article du 27 octobre, notait qu'aucun examen indépendant complet n'avait été publié et qu'il n'avait pas pu vérifier que la preuve se recompile. Yoseph Franco, du site Arncof, n'a trouvé ni recompilation extérieure ni réaction des responsables de Lean ou de Mathlib ; il relève que le fil d'Axiom sur X évoquait 50 millions de lignes et des centaines d'errata, contre 43,1 millions et 34 écarts dans le billet, et que beaucoup de messages enthousiastes venaient de proches de l'entreprise. Lean contrôle chaque déduction, mais il revient à des humains de confirmer que l'énoncé formel exprime bien la classification, un examen qu'Axiom a elle-même sollicité auprès des spécialistes des groupes et de la communauté Lean.