Axiom, une entreprise d'IA spécialisée dans les mathématiques, annonce que son essaim d'agents AxiomProver a achevé en 24 jours la formalisation en Lean du théorème de classification des groupes simples finis (CFSG), et affirme qu'il s'agit de la première démonstration complète de ce théorème vérifiée par ordinateur. Le code est publié sur GitHub sous licence Apache-2.0. Le dépôt indique que la version finale ne contient aucun marqueur sorry, n'utilise pas native_decide et ne repose que sur trois axiomes standard : l'extensionnalité propositionnelle, l'axiome du choix classique et la correction des quotients.
La classification des groupes simples finis est souvent appelée « le tableau périodique de la symétrie ». Elle établit que tout groupe simple fini appartient soit à l'une des 18 familles infinies, soit à l'un des 26 groupes sporadiques. La preuve d'origine est dispersée dans plus de 500 articles, soit environ 15 000 pages, rédigés par une centaine de mathématiciens entre 1955 environ et 2004. Le dernier morceau, la partie quasithin d'Aschbacher et Smith, occupe à lui seul 1221 pages.
Ce qui s'est passé pendant ces 24 jours
D'après le récit publié par Axiom, le projet a créé son groupe de collaboration Slack le 1er octobre, et les premiers agents sont entrés en service le 2 octobre. L'ensemble de la preuve a été découpé en 108 jalons et environ 380 petites tâches ; les agents s'attribuaient des tâches via des issues GitHub et rendaient compte de leur avancement sur Slack. Un agent principal découpait les problèmes et relisait les énoncés, tandis que les autres cherchaient des résultats existants ou rédigeaient des preuves Lean, en redistribuant du travail vers le bas lorsqu'il manquait des prémisses.
Le déroulement n'a pas été fluide. Un premier lot de code a été entièrement supprimé à cause d'erreurs liées à des hypothèses implicites, et l'équipe a dû replanifier. Plus tard, la vitesse de compilation est devenue le goulot d'étranglement : les ingénieurs ont eu recours au cache et à la vérification en parallèle, et ont externalisé les calculs finis sous forme de certificats vérifiables, ramenant la compilation complète sous les 24 heures. Le 10 octobre, le projet avait annoncé séparément la démonstration que le groupe Monstre est simple.
Côté corpus, Axiom indique avoir lu au total 715 articles et ouvrages, et réutilisé environ 1,2 million de lignes de code du projet antérieur Qiuzhen-CFSG, ainsi que des bibliothèques de formalisation existantes comme Mathlib et Tau Ceti.
Des erreurs repérées au passage
Au cours de la formalisation, l'équipe a consigné 34 écarts mathématiques assez nets. Le plus remarqué se situe sur la voie du « théorème des groupes déséquilibrés » (UGT) : une affirmation sur les clôtures dans les mémoires de Walter de 1986 admet un contre-exemple, puisqu'en partant de PSL₂(49) on aboutit à PSL₂(7), précisément exclu de cette famille. Un lemme d'Aschbacher et Smith a lui aussi livré un contre-exemple, SL₂(5) ; une fois l'égalité remplacée par une inégalité, l'argumentation qui suit doit être étendue en conséquence.
Axiom a publié à ce sujet un article distinct de 35 pages, qui propose un argument de remplacement, et a réparé cette voie avec la participation de conseillers tels que Lyons et Solomon. L'entreprise insiste à plusieurs reprises sur le fait que ces contre-exemples ne réfutent pas l'UGT lui-même, et encore moins ne remettent en cause la classification.
« the classification remains the achievement of the mathematicians who discovered the groups »
(La classification reste l'œuvre des mathématiciens qui ont découvert ces groupes.)
Comparaison avec les vérifications mécaniques précédentes
En comparaison horizontale, la référence la plus souvent citée est la vérification du théorème de l'ordre impair achevée en 2012 par l'équipe de Gonthier dans Coq. Ce théorème découle de l'article de 255 pages de Feit et Thompson de 1963 ; le projet a duré environ six ans et constitue une pierre angulaire de la démonstration de la classification. Axiom couvre cette fois l'édifice entier, et la durée se compte en jours.
Les deux vitesses ne sont pas directement comparables. Le projet de l'ordre impair avait bâti sa bibliothèque presque à partir de zéro, tandis qu'Axiom s'appuie sur Mathlib et sur les 1,2 million de lignes de code CFSG antérieures ; le nombre d'agents n'est décrit que comme « plusieurs dizaines », et la puissance de calcul, le matériel et le coût total qui sous-tendent l'ensemble n'ont pas été divulgués, pas plus que les heures de travail humain. Les 24 jours correspondent à la durée du projet de formalisation lui-même et n'incluent pas les décennies de travail humain dont il dépend.
Plusieurs réserves sont également exposées clairement. Les métadonnées du projet qualifient la relecture d'« auto-évaluation », et aucun tiers n'a pour l'instant reproduit la compilation complète depuis un environnement vierge. La vérification par machine garantit seulement que la déduction est valide à partir des hypothèses écrites ; savoir si les définitions de l'énoncé de classification sont fidèles au théorème d'origine exige encore que des spécialistes de la théorie des groupes les confrontent une à une. L'article sur l'UGT a été publié sur une plateforme de prépublication sans évaluation par les pairs, et Axiom dit que la liste des errata sera placée sur la page du projet.
Pour ceux qui travaillent sur la formalisation, la suite se joue sur deux points : la communauté parviendra-t-elle à faire tourner indépendamment ces 43,1 millions de lignes, et combien des 34 écarts seront confirmés par les auteurs d'origine.
Sources : annonce du projet et dépôt GitHub d'Axiom, Unite.AI, CocoLoop, Kingy AI ; le nombre de lignes de code Lean, de déclarations, de jalons et d'écarts suit les chiffres publiés par Axiom, et la durée de la vérification du théorème de l'ordre impair provient de documents de Microsoft Research.