Axiom annonce avoir vérifié en Lean la classification des groupes finis simples, la plus longue preuve des mathématiques

La start-up Axiom affirme avoir rendu vérifiable par ordinateur la classification des groupes finis simples (souvent abrégée CFSG), surnommée « le théorème énorme » : une preuve d’environ 15 000 pages, répartie dans plus de 500 articles écrits par une centaine de mathématiciens en plusieurs décennies. L’annonce est tombée sur X ce mardi 27 octobre à 15 h 34, heure de Paris, accompagnée d’un long article de blog daté de la veille, d’une carte de preuve interactive et d’un dépôt de code.

De quoi parle-t-on

Un groupe décrit des symétries, comme les 24 rotations qui laissent un cube inchangé. Les groupes finis se décomposent en « briques » indivisibles, les groupes simples, un peu comme les nombres entiers en nombres premiers. La classification dit que la liste de ces briques est complète : des groupes cycliques d’ordre premier, des groupes alternés (sur au moins cinq éléments), seize familles infinies de groupes « de type de Lie » et exactement 26 groupes sporadiques, dont le plus grand, le groupe Monstre. Ce résultat sert dans de nombreux domaines (algèbre, théorie des nombres, combinatoire), mais très peu de personnes peuvent en vérifier l’ensemble.

Axiom a réécrit cette preuve dans Lean, un assistant de preuve : un langage où chaque définition et chaque étape logique sont écrites assez précisément pour qu’un programme les contrôle. Le site du projet affiche 43,1 millions de lignes de Lean et 2,05 millions de déclarations.

Comment des agents d’IA ont été mis à contribution

Le récit d’Axiom est surtout celui d’une organisation. Le projet démarre le 1er octobre 2026 avec une carte de preuve tirée de la littérature et du code Lean déjà existant, découpée en 108 jalons et environ 380 tâches. Dès le 2 octobre, des essaims de plusieurs dizaines d’agents AxiomProver, utilisant un mélange changeant de modèles, réclament des tâches via des tickets GitHub et rendent compte dans Slack. Des agents « chefs » découpent les arguments difficiles et vérifient les énoncés ; d’autres cherchent des résultats existants ou écrivent les preuves.

Axiom ne cache pas les ratés. Des jalons apparemment simples cachaient d’énormes prérequis que les agents avaient supposés au lieu de les démontrer : des dizaines de milliers de lignes ont été supprimées. Le temps de recompilation est aussi devenu un goulet d’étranglement, réglé par un système de cache partagé entre machines. Les humains restaient au centre : mathématiciens pour les obstacles de fond, ingénieurs pour faire tourner le système.

Ce que la machine a trouvé

Formaliser oblige à expliciter ce qu’un lecteur humain comble de lui-même. Selon Axiom, la plupart des problèmes relevés étaient mineurs (coquilles, tables erronées, hypothèses oubliées), mais 34 écarts notables avec la littérature ont dû être résolus. Le plus sérieux touche le théorème des groupes non équilibrés, dans la version de John Walter de 1986 : les agents ont trouvé des contre-exemples à une étape du raisonnement, sans pour autant réfuter le théorème lui-même. Avec l’aide de Richard Lyons et Ronald Solomon, deux spécialistes historiques de la classification, une autre route a été construite à partir de travaux de Solomon de 1976. Axiom la présente comme un nouveau résultat de théorie des groupes, décrit dans un article qui accompagne la publication.

Axiom promet de publier la liste complète d’errata avec un comité de spécialistes. Tant qu’elle n’est pas en ligne, le nombre total d’erreurs relevées reste invérifiable.

Les limites à garder en tête

Lean contrôle les déductions, pas le sens de l’énoncé : il faut encore que des humains vérifient que le théorème final et ses définitions disent bien ce que dit la classification. Axiom le reconnaît dans son texte. À l’heure où nous écrivons, aucune vérification indépendante complète n’a été publiée et nous n’avons pas recompilé nous-mêmes le dépôt. La formalisation ne part pas non plus de zéro : elle intègre environ 1,2 million de lignes du projet Qiuzhen-CFSG et s’appuie sur la bibliothèque Mathlib.

Cette annonce arrive au lendemain des résultats mathématiques revendiqués par OpenAI, que nous avons présentés ici. La démarche est différente : OpenAI dit avoir trouvé des résultats nouveaux, Axiom dit avoir vérifié mécaniquement un résultat connu et en avoir corrigé des morceaux.