Axiom formalise le Stacks Project en Lean avec l'IA

Axiom Math, startup spécialisée dans la formalisation mathématique par intelligence artificielle, a publié le 4 novembre 2026 une version codée et vérifiable du Stacks Project, la référence ouverte d’algèbre géométrique développée depuis vingt ans par plus de 650 contributeurs sous la direction de Johan de Jong, de l’université Columbia. Composé de 116 chapitres, de plus de 7 600 pages et de plus de 20 000 définitions, lemmes et théorèmes interdépendants, ce projet est souvent présenté comme la Wikipédia de l’algèbre géométrique. La formalisation, réalisée avec le langage de preuve Lean et s’appuyant sur le catalogue Mathlib, comprend environ 15,75 millions de lignes de code. Elle dépasse les travaux antérieurs d’Axiom par sa nature moins ponctuelle. Après la preuve du résultat sur l’intervalle entre les nombres premiers et la formalisation de la classification des groupes simples finis, la startup passe à une base vivante, destinée à être consultée, corrigée et enrichie en continu. Le système est organisé en deux niveaux : une partie centrale validée humainement, conforme aux normes de Mathlib, et une partie avancée produite par des agents d’IA, chacune des preuves étant contrôlée par le noyau de Lean. Axiom indique avoir coordonné des agents comme dans un projet d’ingénierie : conception globale, écriture des définitions et génération de preuves. Des dizaines d’affirmations du texte original ont dû être corrigées localement, et des contre-exemples ont été produits pour certaines affirmations fausses. Chaque étiquette du Stacks Project renvoie désormais au code Lean et à ses dépendances, permettant de suivre la chaîne logique jusqu’aux fondements. Johan de Jong a toutefois demandé que les contributions automatiques ne remontent pas directement dans le dépôt officiel du projet ; la base reste donc hébergée par Axiom. Cette initiative ravive le débat sur la valeur des grandes formalisations automatiques. Fin septembre, Anthropic avait déjà produit une formalisation en Lean du dernier théorème de Fermat en une douzaine de jours, avec plus de 13 millions de lignes. Plusieurs membres de la communauté Lean, dont Kevin Buzzard, mettent en garde : sans usage par les mathématiciens ni respect des standards, une preuve générée par IA peut n’avoir qu’une portée limitée. Les critiques portent surtout sur la revue humaine, devenue le principal goulot d’étranglement, et sur la difficulté pour une machine de vérifier que le code exprime fidèlement l’intention mathématique, et pas seulement la validité des étapes de déduction. Pour réduire ce goulet, des projets comme Tau Ceti testent une revue automatisée en adversaire, où une IA produit du code et une autre le vérifie selon des règles fixées par des experts. Malgré ces innovations, le consensus reste que la confiance pleine nécessitera encore un contrôle humain. À plus long terme, les artisans de cette filière estiment qu’une grande partie des mathématiques pourrait être formalisée sous trois ans, transformant non seulement la vérification des preuves, mais aussi la manière dont les mathématiciens rédigent et corrigent leurs raisonnements.