Axiom Math a vérifié 16 millions de lignes de code Lean avec des agents et comblé une lacune des mathématiques formelles

Alors que l'IA « résout » chaque semaine un nouveau problème mathématique, une question légitime se pose : qui vérifie tout cela ? Rien que le mois dernier, OpenAI a publié 719 manuscrits annonçant des solutions à des problèmes difficiles. Il est impossible de tous les lire à la main, et des erreurs passent même à travers les vérifications automatiques. La start-up Axiom Math, valorisée 1,6 milliard de dollars, propose une autre voie : ne pas ralentir, mais s'appuyer sur un socle vérifié.

Ce qui a été fait

Mercredi, l'entreprise a annoncé avoir vérifié formellement le Stacks Project, l'un des plus vastes corpus de mathématiques humaines de l'histoire. Il a été lancé en 2005 par Johan de Jong, de l'université Columbia, comme ouvrage de référence ouvert. Il compte aujourd'hui environ 7 654 pages : de l'algèbre de niveau universitaire aux idées de pointe de la géométrie algébrique et de la théorie des nombres.

Les agents d'Axiom ont réécrit l'ensemble sous la forme d'environ 16 millions de lignes de code dans le langage Lean. Ensuite, un programme appelé proof assistant a vérifié le code ligne par ligne. Si la vérification réussit, la preuve est logiquement correcte et il n'est plus nécessaire de croire l'auteur sur parole.

Pourquoi c'est plus difficile qu'il n'y paraît

Vérifier chaque théorème isolément ne fait que la moitié du travail. Les résultats du Stacks sont reliés comme un arbre généalogique : chacun s'appuie sur les précédents. Si une définition « dérive » quelque part, tout ce qui se trouve au-dessus s'effondre. L'équipe devait donc préserver toutes les connexions sur 16 millions de lignes. La CEO Carina Hong reconnaît elle-même qu'elle n'était pas sûre de réussir au départ : ce qui est grand et fragile fait rarement bon ménage.

L'architecture était la suivante : une hiérarchie souple au sommet, sans répartition rigide des tâches. Les agents trouvaient eux-mêmes sur quoi travailler et opéraient en parallèle. Axiom a aussi entraîné ses propres modèles pour les mathématiques, ce que, selon Hong, la plupart de ses concurrents en vérification ne font pas. Au début, un expert Lean interne inculquait aux agents un « goût », c'est-à-dire une compréhension de ce à quoi ressemble du bon code. Avec le temps, dit Hong, ils sont devenus autonomes.

Pourquoi cela intéresse les développeurs

L'intérêt pratique ne réside pas dans la géométrie algébrique elle-même. La vérification formelle est depuis longtemps utilisée là où une erreur coûte cher : la vérification de puces, et des chercheurs français s'en sont servis pour trouver des bugs dans un logiciel de calcul des allocations familiales. Le problème est que les agents écrivent de plus en plus de code, sans que les garanties d'absence de bugs et de failles de sécurité augmentent.

Le pari d'Axiom : les mathématiques sont un terrain d'entraînement où cette compétence se perfectionne, avant d'être transposée au logiciel. Les agents peuvent lire une bibliothèque Lean existante et bâtir du neuf dessus, sans repartir de zéro. Terence Tao formule le principe général ainsi : plus il y a de preuves formalisées, plus on peut en produire de nouvelles.

Limites

Pour l'instant, il s'agit d'une déclaration de l'entreprise elle-même, et l'article ne mentionne aucune évaluation indépendante. Le transfert de cette compétence des mathématiques au code industriel est une hypothèse, pas un fait démontré. Les logiciels réels dépendent de l'environnement, des dépendances et d'exigences informelles qui ne se formalisent pas aussi proprement que des théorèmes. L'appel de Hong à toutes les entreprises qui écrivent du code à se lancer dans la formalisation à cette échelle sonne fort, mais relève pour l'instant plutôt du marketing.

Que faire en pratique

Si vous concevez des systèmes d'agents pour le code, intéressez-vous à Lean et à l'idée d'artefacts vérifiables : que l'agent produise non seulement du code, mais aussi ce qui peut être contrôlé automatiquement. Pour les product managers, la conclusion est plus simple : « écrit par l'IA » et « écrit par l'IA et prouvé » deviendront bientôt deux catégories de qualité distinctes. Pour ceux qui travaillent dans des domaines critiques — finance, santé, sécurité —, ce basculement mérite d'être surveillé dès maintenant.