Axiom formalise Stacks, socle mathématique vérifié pour l'IA
Axiom Math, startup valorisée 1,6 milliard de dollars, a annoncé mercredi avoir formellement vérifié le Stacks Project, l’une des plus grandes bibliothèques mathématiques jamais rédigées par des humains, en le traduisant en plus de 16 millions de lignes de code vérifiables par la machine. L’objectif est d’offrir aux systèmes d’intelligence artificielle une base logique suffisamment solide pour écrire du logiciel, puis, à terme, faire de la science sans multiplier les erreurs invérifiables. Fondée en mars 2025 par Carina Hong, 25 ans, après son départ d’un doctorat en mathématiques à Stanford, Axiom a levé 200 millions de dollars lors d’un tour Série A mené par Menlo Ventures. L’entreprise part d’un constat simple: la production de résultats par des modèles d’IA croît très vite, OpenAI ayant publié le mois dernier 719 manuscrits revendiquant des solutions à des problèmes difficiles, sans que la machine garantisse toujours leur justesse. Pour éviter que les mathématiques ne sombrent dans le “slop” algorithmique, Axiom mise sur la formalisation. Le procédé consiste à traduire des preuves humaines dans Lean, un langage de programmation conçu pour le raisonnement mathématique. Un assistant de preuve analyse ensuite le code ligne par ligne. Si la preuve est acceptée, elle peut être considérée comme logiquement correcte, au moins dans le cadre formel choisi. Le Stacks Project, créé en 2005 par le mathématicien Johan de Jong comme référence ouverte et souvent comparé à la série Bourbaki, contenait environ 7 654 pages couvrant l’algèbre, la géométrie et la théorie des nombres. Ses résultats étant fortement imbriqués, chaque définition ou théorème en dépend d’autres; la difficulté ne tenait donc pas seulement au volume, mais à la préservation de toutes ces connexions. Pour relever le défi, Axiom a déployé une flotte d’agents IA travaillant en parallèle, capables de sélectionner des tâches elles-mêmes dans une hiérarchie de travail laissée volontairement souple. L’entreprise a aussi entraîné ses propres modèles spécialisés, avec l’aide d’experts internes en Lean, afin de transmettre une forme de “goût” mathématique à ses systèmes. Le projet est perçu comme un jalon parce qu’il comble une lacune majeure dans la formalisation des mathématiques, notamment en géométrie algébrique, où les chercheurs disposaient jusqu’ici de peu d’éléments vérifiés pour s’appuyer sur Lean. Pour Axiom, l’enjeu dépasse les mathématiques. Comme les agents IA écriront de plus en plus de code, les développeurs auront besoin de fondations vérifiées pour limiter bugs et failles de sécurité. Les résultats formalisés peuvent ensuite servir de briques réutilisables: chaque théorème vérifié en aide d’autres. Terence Tao a résumé cette logique en soulignant qu’une plus grande formalisation permet d’en produire davantage. Carina Hong y voit une condition pour empêcher les IA de reproduire des choix d’ingénierie hasardeux: sans bibliothèque fiable, leur capacité à étendre les connaissances risque de se fragiliser plutôt que de s’améliorer.
