Preuve d’Axiom : ce que ça change pour la superintelligence

Avancées technologiques · 29 octobre 2026

La preuve d'Axiom est une première : la start-up Axiom Math dit avoir fait vérifier par ordinateur, en 24 jours et avec des essaims d'agents IA, la classification des groupes simples finis, une démonstration de 15 000 pages, la plus longue des mathématiques. Pour la superintelligence, c'est un test grandeur nature : des agents IA capables de mener, sous direction humaine, un chantier de raisonnement géant, et d'y trouver des erreurs.

Cet article explique simplement ce qui a été fait, ce qui reste à vérifier et ce que cette preuve mathématique par IA change pour le débat sur la superintelligence. Les chiffres viennent d'Axiom et n'ont pas encore été reproduits par une équipe extérieure.

Qu'est-ce que la preuve d'Axiom ?

La classification des groupes simples finis, surnommée « théorème énorme », dresse la liste complète des « briques » de base de la symétrie en mathématiques : des familles infinies et 26 groupes isolés dits sporadiques, dont le célèbre groupe Monstre. Sa démonstration s'étale sur environ 15 000 pages, plus de 500 articles et une centaine de mathématiciens, sur plusieurs décennies.

Le 26 octobre 2026, Axiom Math a annoncé l'avoir entièrement formalisée dans Lean, un logiciel qui vérifie chaque étape d'une démonstration. Selon son blog :

• environ 43,1 millions de lignes de Lean et 2,05 millions de déclarations ;
• 108 grandes étapes et environ 380 tâches, réalisées entre le 2 et le 25 octobre ;
• le code est publié sous licence Apache 2.0, et une compilation complète prend moins de 24 heures (Unite.AI) ;
• la version formalisée est la preuve dite « de première génération » ; la seconde, plus moderne, est elle-même inachevée.

Comment des agents IA ont-ils écrit cette preuve mathématique ?

Axiom a fait travailler des « essaims » de dizaines d'agents IA pilotés par son système AxiomProver :

• des agents chefs découpaient les arguments et relisaient les énoncés ;
• d'autres cherchaient les résultats existants ou rédigeaient les preuves en Lean ;
• les agents pouvaient déléguer un lemme manquant à un autre agent, via un dépôt partagé ;
• les calculs finis très lourds ont été sortis sous forme de certificats vérifiables à part.

Les humains ont joué un rôle de direction : des mathématiciens analysaient les blocages et relisaient les rapports importants, et des spécialistes du domaine, Richard Lyons et Ronald Solomon, ont été consultés. Axiom ne précise ni les modèles utilisés ni la puissance de calcul.

Des erreurs trouvées dans la littérature

Le résultat le plus parlant n'est pas la taille de la preuve, mais ce que les agents ont trouvé en chemin. Axiom recense 34 écarts notables avec les publications : surtout des coquilles, des erreurs de tables ou des hypothèses oubliées. Deux cas sont plus sérieux :

• un lemme d'Aschbacher et Smith affirmait une égalité fausse : les agents ont trouvé un contre-exemple ;
• une étape du théorème des groupes non équilibrés (UGT) de Walter était fausse ; la réparation s'appuie sur un nouveau résultat produit avec AxiomProver, décrit dans un article de Colin Defant et Ken Ono.

Axiom souligne que la classification elle-même n'a jamais été remise en cause : les trous ont été comblés.

Ce qui reste à vérifier

• Personne ne l'a encore refaite. La PDG Carina Hong a répondu « pas encore » à la question d'une reconstruction indépendante ; Axiom publie les fichiers pour l'encourager (RuntimeWire, 27 octobre).
• Lean vérifie la logique, pas l'énoncé. Des humains doivent confirmer que les définitions formelles disent bien ce que disent les mathématiciens.
• Les certificats de calcul doivent être vérifiés séparément.
• Le nouveau résultat sur l'UGT est publié en prépublication ; Axiom ne mentionne pas de relecture par les pairs.

Plus largement, la BBC a relayé le 28 octobre les inquiétudes de mathématiciens sur la nouveauté réelle des découvertes attribuées aux IA et sur la capacité des revues à suivre (selon le résumé de The Neuron).

Ce que ça change pour la superintelligence

La super intelligence artificielle désigne une IA qui dépasserait les meilleurs humains dans presque tous les domaines (voir notre guide super intelligence artificielle : définition simple). La preuve d'Axiom n'en est pas une, mais elle apporte trois signaux :

• Des tâches très longues. Coordonner des centaines de sous-tâches sur trois semaines est ce que les chercheurs attendent d'agents autonomes avancés.
• Une vérification automatique. Avec Lean, on n'a pas à croire l'IA sur parole : c'est une piste concrète pour contrôler des systèmes plus forts que nous, au cœur de l'alignement.
• Une accélération de la science. Après les annonces d'OpenAI sur ses résultats en mathématiques et les preuves formelles de Claude sur des logiciels open source, les mathématiques deviennent le terrain d'essai de l'IA de recherche.

Prudence toutefois : cette réussite concerne un domaine où chaque étape se vérifie mécaniquement. Rien ne dit qu'elle se transpose à des domaines flous comme la stratégie ou la biologie. Toute date d'arrivée de la superintelligence reste une prévision.

FAQ

Conclusion

En 24 jours, des agents IA ont fait vérifier par machine ce qu'une centaine de mathématiciens avaient bâti en décennies, et y ont trouvé des erreurs. Le vrai test sera la reproduction indépendante. Retrouvez les autres progrès sur nos avancées IA et les notions de base dans la FAQ.