Axiom Math formalise en 24 jours le « théorème énorme » : 43,1 millions de lignes de Lean

Axiom Math annonce avoir terminé la vérification par ordinateur du théorème de classification des groupes simples finis (CFSG), que les mathématiciens appellent le « théorème énorme ». En 24 jours, des dizaines d'agents IA ont écrit environ 43,1 millions de lignes de code Lean et formalisé une preuve qui occupe 15 000 pages réparties dans plus de 500 articles scientifiques. Environ 100 chercheurs y ont travaillé pendant des décennies. Axiom présente ce résultat comme la première preuve complète du CFSG vérifiable par ordinateur. Le code et les matériaux sont publiés pour un examen indépendant.

Une table périodique des symétries

Le moyen le plus simple de comprendre ce que classifie le théorème, c'est le cube. On peut le faire pivoter de 24 façons différentes pour qu'il reste exactement identique. Ces rotations forment un groupe mathématique. Le CFSG décrit les « briques » fondamentales à partir desquelles sont construits tous les groupes finis de symétries. Il en résulte une sorte de table périodique des symétries, utilisée en algèbre, en théorie des nombres et en physique mathématique.

Le problème tient à la manière dont cette preuve a été établie. Des auteurs différents l'ont assemblée morceau par morceau, au fil de plusieurs décennies, dans des centaines d'articles. Un humain peut difficilement la revérifier en entier : il faudrait garder en tête des milliers de lemmes interdépendants, dispersés dans des revues. La formalisation en Lean lève cet obstacle. Chaque étape du raisonnement est écrite sous forme de code, et le noyau de Lean vérifie mécaniquement que la conclusion découle bien des étapes précédentes.

L'arithmétique du projet : 43 millions de lignes en 24 jours

Les chiffres donnent l'échelle. 43,1 millions de lignes en 24 jours représentent de l'ordre de 1,8 million de lignes par jour, soit environ 75 mille par heure en comptant 24 heures sur 24. Chaque page de la preuve papier correspond à environ 2 900 lignes de code formel. La formalisation est détaillée à un tout autre niveau que le texte original, car dans leurs articles les mathématiciens sautent les étapes « évidentes », ce que Lean n'autorise pas.

Il s'agit d'un travail d'agents, pas d'une seule longue génération. Des dizaines d'agents ont mené des branches de formalisation en parallèle, et le code final devait converger vers une seule preuve acceptée par le noyau vérificateur. C'est cette vérification par le noyau qui distingue un tel résultat de la sortie habituelle d'un modèle de langage : une étape erronée ne passe tout simplement pas.

Ce que les agents ont trouvé en cours de route

La formalisation a apporté non seulement une confirmation, mais aussi de nouvelles découvertes. Axiom énumère les résultats suivants :

• environ 43,1 millions de lignes de code Lean, produites en 24 jours par des dizaines d'agents IA ;
• 34 écarts significatifs avec les travaux mathématiques publiés ;
• des contre-exemples à certains énoncés de la littérature, ainsi que des preuves alternatives pour ces énoncés ;
• un nouveau résultat en théorie des groupes, nécessaire au chemin de preuve retenu ;
• dans certains cas, des erreurs découvertes dans les raisonnements d'origine, et de nouveaux arguments mathématiques qui les corrigent ;
• un travail conjoint avec des mathématiciens, dont des spécialistes ayant participé à la classification initiale.

La participation humaine reste ici essentielle. Quand la formalisation bute sur un écart avec une publication, il faut un expert pour distinguer une coquille d'une véritable faille. L'expérience des auteurs de la classification initiale a aidé à déterminer où la version formelle devait suivre l'original et où il fallait emprunter un autre chemin.

Ce que l'industrie peut en retenir

La principale leçon pour l'industrie : des agents qui écrivent et auto-vérifient du code dans un environnement doté d'un vérificateur strict peuvent venir à bout de tâches hors de portée du travail manuel. Lean joue ici le rôle d'un juge qui ne croit sur parole ni les humains ni le modèle. Le même schéma s'applique à tout domaine où le résultat peut être vérifié automatiquement : vérification de logiciels critiques, de protocoles, de constructions cryptographiques.

Une mise en garde s'impose néanmoins. La vérification par ordinateur garantit que la preuve est correcte au regard des définitions et des formulations écrites. C'est pourquoi l'ouverture du code compte autant que le résultat lui-même : les mathématiciens pourront lire les définitions et s'assurer que c'est bien ce qu'il fallait qui a été formalisé. Axiom ne donne pas, dans son annonce, le coût d'une telle exécution (calcul et tokens). Or c'est ce chiffre qui dira si la revérification formelle de résultats fondamentaux deviendra une routine ou restera un projet isolé.

Pour les mathématiciens, le signal est clair. La littérature qu'il fallait jusqu'ici accepter par confiance envers l'autorité se prête désormais à une revérification mécanique complète, et 34 écarts significatifs ont déjà été trouvés sur ce chemin.