Contexte et enjeux
Axiom Math, startup évaluée à 1,6 milliard $, a annoncé la formalisation complète du Stacks Project, une référence open source de 7 654 pages couvrant l’algèbre, la géométrie algébrique et la théorie des nombres. La démarche intervient après la diffusion massive de manuscrits générés par l’IA – 719 publications le mois dernier – dont la fiabilité reste incertaine. En s’appuyant sur une bibliothèque mathématique reconnue comme « l’équivalent moderne des Bourbaki », Axiom vise à fournir une base vérifiable pour les agents d’IA qui écrivent du code ou conduisent de la recherche scientifique.
Processus de formalisation
Les équipes d’Axiom ont converti le texte du Stacks Project en environ 16 millions de lignes de code Lean, le langage de preuve assistée. Chaque théorème a été réécrit en Lean puis soumis à un assistant de preuve qui vérifie chaque ligne de façon exhaustive. La complexité provient de l’interdépendance des résultats : les définitions et les lemmes s’enchaînent comme un arbre généalogique, exigeant que chaque connexion soit préservée. Les agents d’IA ont travaillé en parallèle, recevant une hiérarchie souple plutôt qu’une instruction détaillée, ce qui a permis d’identifier des tâches indépendantes et de les exécuter simultanément.
Analyse technique et limites
Le choix de Lean repose sur sa capacité à exprimer des preuves de façon constructive, comparable aux vérifications formelles utilisées en ingénierie de puces. Cependant, la traduction massive implique des risques de divergence entre le texte original et le code, notamment lorsqu’une définition ambiguë doit être interprétée. Axiom a atténué ce problème en formant ses propres modèles de langage spécialisés en mathématiques, puis en les faisant « goûter » les standards humains via un expert interne. Malgré ces précautions, la vérification ne garantit pas l’absence de lacunes conceptuelles : elle ne valide que la logique formelle, pas la pertinence mathématique au sens large.
Implications pour l’IA et le développement logiciel
Une fois formalisés, les résultats du Stacks Project constituent des blocs de construction réutilisables. Les futurs agents d’IA pourront invoquer ces lemmes comme des fonctions vérifiées, réduisant le besoin de reconstruire des preuves à chaque itération. Cette approche s’aligne avec les pratiques de vérification formelle en DevOps, où la sécurité et la robustesse du code sont essentielles. En outre, la démarche d’Axiom, soutenue par une levée de fonds de 200 M$ en série A dirigée par Menlo Ventures, propose un modèle où la formalisation à grande échelle devient un service exploitable par les développeurs et les chercheurs, limitant le « slop » généré par les systèmes d’IA autonomes.
