TL;DR
- Axiom a publié la première preuve complète, vérifiée par machine, de la Classification des groupes simples finis, ce résultat d’environ 15 000 pages connu sous le nom de « l’énorme théorème » : 43,1 millions de lignes de Lean, 2,05 millions de déclarations, construits en 24 jours par des essaims de dizaines d’agents IA dirigés par ses ingénieurs et mathématiciens.
- La formalisation a mis au jour 34 écarts notables par rapport à la littérature publiée, dont le pire était un contre-exemple qui invalidait la voie publiée standard vers le théorème des groupes non équilibrés (Unbalanced Group Theorem). Axiom a remplacé l’étape défaillante par un théorème que son prouveur a trouvé, formalisé et rédigé.
- Les modes de défaillance de l’essaim constituent la partie utile. Les agents supposaient les prérequis au lieu de les prouver, des dizaines de milliers de lignes ont dû être supprimées et des parties du plan relancées, et la progression était si irrégulière qu’un jalon n’a été clos que le 13 octobre.
- La contrainte limitante n’a jamais été la capacité du modèle. C’était la capacité de Lean à revérifier ce que les agents avaient écrit — et, à la fin, l’humain qui confirme que l’énoncé formel correspond bien au théorème qui intéressait tout le monde.
Ce qui a réellement été livré
Axiom a publié la version le 26 octobre. L’objet en question est la classification qui donne une liste complète des « atomes » de la symétrie finie — les groupes cycliques d’ordre premier, les groupes alternés, seize familles infinies de type Lie, et exactement 26 groupes sporadiques. Sa preuve originale est la plus longue des mathématiques : « environ 15 000 pages réparties dans plus de 500 articles rédigés par une centaine de mathématiciens, ce qui a valu à la CFSG le surnom de “l’énorme théorème” ». (Source : Axiom — Formalizing the Enormous Theorem)
Face à cela, le tableau de bord du projet rapporte 43,1 M de lignes de Lean, 2,05 M de déclarations et un corpus de 715 articles et ouvrages. (Source : CFSG in Lean — project dashboard)
Une remise honnête s’impose : environ 1,2 million de ces lignes proviennent de la formalisation antérieure Qiuzhen-CFSG. Il reste tout de même environ 42 millions de lignes de Lean nouvelles en trois semaines et demie. La formulation d’Axiom elle-même : « En 24 jours, les ingénieurs et mathématiciens d’Axiom Math ont dirigé des essaims de dizaines d’agents IA dans un projet qui a produit environ 43,1 millions de lignes de code dans l’assistant de preuve Lean. »
L’essaim était un marché de tâches, pas un pipeline
La conception de la coordination est l’élément transférable. Axiom a ouvert un canal Slack le 1er octobre, assemblé une carte de la preuve à partir de la littérature, et découpé le travail en 108 jalons et environ 380 tâches plus petites. « Un agent pouvait revendiquer une tâche, localiser les arguments pertinents et commencer à les traduire en Lean. Lorsqu’une tâche exigeait des mathématiques qui n’avaient pas encore été formalisées, il pouvait déléguer ces prérequis à d’autres agents. » Les revendications passaient par des issues GitHub, les rapports d’achèvement par Slack, et des agents chefs décomposaient les arguments difficiles pendant que d’autres cherchaient des résultats existants. (Source : Axiom)
La chronologie est inhabituellement détaillée pour ce type d’annonce, et c’est précisément ce qui la rend plus crédible qu’un graphique de benchmark. Premier essaim en activité le 2 octobre. Le 10 octobre, un message est arrivé dans le canal : « WE PROVED MONSTER IS SIMPLE. » Le 13 octobre, un jalon a été clos.
Le mode de défaillance qui compte : la dette d’hypothèses
Le passage le plus instructif de tout l’article porte sur ce qui a mal tourné :
« Certains jalons apparemment gérables dissimulaient d’énormes prérequis, que les agents avaient supposés plutôt que prouvés. Nous avons supprimé des dizaines de milliers de lignes bâties sur ces hypothèses et relancé des parties du travail selon un plan plus solide. »
C’est l’équivalent multi-agents d’une compilation qui passe contre un mock. Un agent qui a besoin d’un lemme peut le prouver ou le supposer, et dans un essaim de dizaines de travailleurs, la solution de facilité est toujours de supposer — localement valide, globalement mortel. Axiom nomme directement le problème de revue : « Une difficulté récurrente consistait à déterminer si l’ajout d’une hypothèse à un théorème reportait du travail ou en changeait le sens. »
C’est pourquoi les décomptes de jalons mentent. « Compter les résultats achevés aidait à organiser le travail, mais la formalisation n’était complète que lorsque les pièces formaient une preuve unique sans hypothèses injustifiées restantes. » Remplacez « jalons clos » par « tickets clos » et le paragraphe reste vrai pour n’importe quelle flotte d’agents.
34 écarts, un nouveau théorème
La formalisation force chaque étape implicite à se révéler, et la littérature de la CFSG en regorgeait. Axiom rapporte 34 écarts notables après filtrage des coquilles, erreurs de tableaux et hypothèses omises. Le plus important se trouvait dans le théorème des groupes non équilibrés, qu’il formalisait à travers le mémoire de John Walter de 1986 : « nos agents ont trouvé des contre-exemples explicites à une assertion de fermeture utilisée dans la preuve de Walter… Cela laissait une inférence clé injustifiée, mais les contre-exemples ne réfutaient pas l’objectif visé du UGT. » (Source : Axiom)
Le contre-exemple est vérifiable à la main : prenez PSL₂(49), dont l’involution de corps a pour centralisateur PGL₂(7), dont la composante simple PSL₂(7) sort de la famille de Walter parce que 7 est un nombre premier de Mersenne.
Axiom ne l’a pas masqué. Après consultation de Richard Lyons et Ronald Solomon, son prouveur a produit et formalisé un argument alternatif fondé sur la théorie des 2-composantes maximales de Solomon (1976) ; le nouveau théorème 2.3, « Preservation of simple tops », se présente désormais comme un résultat de théorie des groupes à part entière. (Source : Axiom — The Unbalanced Group Theorem)
Deux découvertes plus modestes méritent une ligne. Un lemme des volumes sur les groupes quasiminces d’Aschbacher et Smith affirmait l’égalité de deux quantités ; les agents ont trouvé un contre-exemple dans SL₂(5) où l’une vaut 1 et où l’égalité exigerait 2, et des scissions de cas en aval s’appuyaient dessus. Et après la formalisation, les mathématiciens d’Axiom ont trouvé une voie de première génération plus courte qui contourne entièrement le théorème 2.3 — la remarque 9.5 de l’article, conservée aux côtés de l’argument machine plus long.
Le goulot d’étranglement fut le vérificateur, puis la spécification
« À mesure que le dépôt grossissait, les temps de compilation sont devenus un goulot d’étranglement : les agents produisaient des preuves plus vite que Lean ne pouvait les revérifier, et modifier un résultat partagé pouvait forcer Lean à revérifier tous ses dépendants. » La réponse d’Axiom fut infrastructurelle, non liée au prompting : mise en cache distribuée des résultats de compilation entre les workers, vérifications indépendantes en parallèle, et calculs finis coûteux externalisés en certificats vérifiables séparément — une vérification « de plusieurs ordres de grandeur » plus rapide.
Puis la limite se déplace. « Des humains inspectent cet énoncé et les définitions qu’il utilise pour confirmer qu’il exprime la classification visée ; Lean vérifie les déductions formelles qui l’établissent. »
Lisez cela comme une loi générale du travail agentique, et non comme une note de bas de page mathématique. Un vérificateur qui passe certifie que la machine a fait ce que disait la spécification ; il ne dit rien sur la question de savoir si la spécification est ce que vous vouliez. La CFSG en est la version bénigne de cet écart — Axiom affirme que ses humains ont formalisé le théorème visé, et gère les errata avec Lyons et Solomon au sein d’un comité consultatif. Le même écart dans un agent de paiement, c’est un incident un vendredi.
Pourquoi cela compte au-delà des mathématiques
Chaque article qui invoque la CFSG en une phrase repose désormais sur un ensemble d’arguments inspectable étape par étape, avec la littérature non résolue documentée plutôt qu’héritée. C’est un artefact durable, et il a coûté moins d’un mois de temps réel.
Trois enseignements survivent à l’effet de nouveauté. Le débit de vérification, et non le débit de génération, fixe le plafond de tout système auto-vérifiant. Les métriques de progression qui comptent les achèvements sont détournées par tout travailleur capable de se frayer un chemin vers le vert par de simples hypothèses. Et la compétence humaine rare se déplace en amont, vers la revue de spécification — le même basculement que la course de 10 000 agents d’OpenAI sur Navier-Stokes, et le même échec que l’étude de DeepMind sur les essaims d’agents a mis au jour une fois les agents récompensés pour un succès déclaré.
FAQ
La preuve de la CFSG est-elle désormais considérée comme vérifiée ? Les déductions le sont : le noyau de Lean a vérifié chaque étape des 43,1 millions de lignes. Ce qui reste humain, c’est de savoir si l’énoncé formel de plus haut niveau capture la classification telle que les mathématiciens la comprennent, et Axiom affirme que des relecteurs l’ont confirmé séparément.
Les agents ont-ils produit de nouvelles mathématiques ? Un nouveau résultat. AxiomProver a produit et formalisé le théorème 2.3, « Preservation of simple tops », utilisé pour remplacer une étape défaillante du théorème des groupes non équilibrés. Le cadrage et le blocage ont été humains.
Quelle part du code préexistait ? Environ 1,2 million de lignes provenaient de la formalisation antérieure Qiuzhen-CFSG, plus la bibliothèque Mathlib. Les quelque 42 millions de lignes restantes ont été produites pendant le projet de 24 jours.
Pourquoi les jalons se sont-ils clos si lentement au milieu du projet ? Ils étaient trop grossiers et masquaient des prérequis. À partir du 13 octobre, les ingénieurs ont mené un effort de replanification qui a découpé les jalons inachevés en théorèmes plus petits et précisément énoncés, chacun devant montrer comment il se recombinait dans la cible initiale.