Axiom Math Vérifie Les Bases Des Mathématiques

Imaginez un instant que les mathématiques, ce pilier millénaire de la rationalité, se mettent à produire des résultats douteux à la chaîne. Chaque semaine, une nouvelle annonce d’intelligence artificielle prétend résoudre un problème ouvert depuis des décennies. Des manuscrits s’accumulent par centaines. Pourtant, même les outils censés valider ces avancées peuvent faillir. Après des années de contenus générés de qualité médiocre, une question s’impose : les mathématiques vont-elles elles aussi succomber au flot de productions approximatives ?

Face à cette menace, une jeune pousse américaine a décidé de ne pas freiner l’innovation, mais de la solidifier. Axiom Math, valorisée 1,6 milliard de dollars, mise sur une fondation formellement vérifiée. L’idée est simple et ambitieuse à la fois : donner aux agents d’intelligence artificielle un socle fiable pour écrire du logiciel et, demain, avancer la science. Mercredi dernier, la société a annoncé avoir formalisé l’intégralité du Stacks Project, l’une des plus vastes collections de mathématiques jamais rédigées par des humains.

Une fondation solide pour les mathématiques de demain

Le Stacks Project occupe une place particulière dans le cœur des mathématiciens. Johan de Jong, professeur à Columbia, l’a lancé en 2005 comme une référence ouverte. Depuis, des contributeurs du monde entier y ont ajouté des résultats allant de l’algèbre de niveau universitaire jusqu’aux concepts les plus avancés en géométrie algébrique et en théorie des nombres. Peter Woit, collègue de de Jong, n’hésite pas à le comparer aux célèbres livres de Bourbaki, cette entreprise monumentale qui a reconstruit les mathématiques sur des bases rigoureuses au XXe siècle.

Axiom Math a transformé ces quelque 7 654 pages en environ 16 millions de lignes de code vérifié par ordinateur. Chaque théorème, chaque définition a été réécrit dans le langage Lean, puis passé au crible par un assistant de preuve. Si le code est accepté, la logique est considérée comme irréprochable. Cette démarche, appelée formalisation, ne se contente pas de vérifier des résultats isolés. Elle préserve toutes les interconnexions, comme un immense arbre généalogique où chaque résultat repose sur ceux qui le précèdent.

Carina Hong, 25 ans, a quitté son doctorat de mathématiques à Stanford pour créer la société en mars 2025. Le même mois, Axiom Math levait 200 millions de dollars en série A, menée par Menlo Ventures. L’équipe n’était pas certaine que l’approche dite de « vibe coding » pourrait préserver la beauté et la cohérence du Stacks Project. Pourtant, le pari a été tenu.

Comment les agents ont collaboré sans chef d’orchestre strict

Pour venir à bout d’un tel volume, les ingénieurs ont donné aux agents une structure hiérarchique souple. Ils n’ont pas dicté chaque tâche. Les agents ont eux-mêmes identifié des portions de travail et se sont organisés en parallèle. Ashvin Swaminathan, membre de l’équipe technique, explique que cette liberté a été déterminante. Les modèles ont progressivement développé leur propre sens du « goût » mathématique, après avoir d’abord été guidés par un expert Lean humain.

Axiom Math a également choisi de former ses propres modèles spécialisés en mathématiques, une stratégie que peu de concurrents dans le domaine de la vérification formelle ont adoptée. Le résultat comble un trou béant : jusqu’ici, la géométrie algébrique restait largement absente des bibliothèques formalisées. Les chercheurs qui souhaitaient vérifier de nouveaux travaux dans ce domaine manquaient de bases. Désormais, ils disposent d’un socle solide.

Terence Tao, médaillé Fields et professeur à UCLA, résume l’intérêt de cette approche avec une formule limpide : plus on dispose de preuves formalisées, plus on peut en produire de nouvelles. Chaque résultat vérifié devient une brique réutilisable. Les agents n’ont plus besoin de repartir de zéro à chaque fois.

Au-delà des mathématiques : sécuriser le code de demain

Les mathématiciens ne sont pas les seuls concernés. Les développeurs peinent depuis longtemps à garantir l’absence de bugs et de failles de sécurité. Le problème s’aggrave à mesure que les agents d’intelligence artificielle écrivent une part croissante du code mondial. Axiom Math parie que le logiciel de demain devra reposer sur des fondations vérifiées, exactement comme le Stacks Project désormais formalisé.

La formalisation n’est pas réservée aux théorèmes abstraits. Les ingénieurs l’utilisent déjà pour valider la conception de puces électroniques. En France, des chercheurs y ont même eu recours pour détecter des erreurs dans des logiciels de calcul des prestations familiales. La même logique peut s’appliquer à grande échelle au code produit par des agents.

Selon Swaminathan, les mathématiques constituent le terrain d’entraînement idéal. La compétence acquise est transférable. Les agents peuvent lire le code Lean formalisé, le comprendre et construire de nouvelles infrastructures par-dessus. Cette bibliothèque devient un substrat réutilisable sur lequel d’autres systèmes peuvent s’appuyer pour repousser les frontières sans accumuler d’erreurs structurelles.

Éviter le piège du mauvais départ

Carina Hong insiste sur un point crucial : si les agents commencent avec des choix d’ingénierie médiocres, il devient extrêmement difficile de corriger le tir par la suite. Une bibliothèque réutilisable bien conçue leur permet de progresser proprement. À l’inverse, un « slop drop » initial compromet tout le développement futur.

L’approche adoptée pour le Stacks Project – agents travaillant en parallèle, choisissant eux-mêmes leurs tâches – préfigure selon elle le mode de fonctionnement dominant de l’intelligence artificielle dans les années à venir. Pour éviter la production massive de contenus approximatifs, il faut fournir aux systèmes un corps de connaissances solide et réutilisable.

Ce que change concrètement cette formalisation

Avant Axiom Math, un chercheur voulant formaliser un résultat en géométrie algébrique devait reconstruire une grande partie des prérequis. Aujourd’hui, il peut s’appuyer sur des millions de lignes déjà vérifiées. Le gain de temps et de confiance est considérable. Les nouvelles preuves deviennent plus accessibles et plus fiables.

La même logique s’applique au développement logiciel. Un agent qui génère du code critique peut s’appuyer sur des composants déjà formalisés plutôt que de réinventer des fonctions élémentaires susceptibles de contenir des failles. La vérification formelle passe d’un exercice académique à une pratique industrielle potentielle.

• Préservation de la cohérence entre des milliers de théorèmes interconnectés
• Création d’une base réutilisable pour la géométrie algébrique et au-delà
• Formation de modèles spécialisés plutôt que simple utilisation d’outils existants
• Organisation autonome des agents sans micro-management strict
• Transfert possible vers la vérification de logiciels critiques

Une levée de fonds qui en dit long sur les ambitions

Lever 200 millions de dollars dès le premier tour, quelques mois après la création, n’est pas anodin. Menlo Ventures a clairement parié sur la capacité d’Axiom Math à devenir une infrastructure essentielle. Dans un contexte où les investissements en intelligence artificielle se concentrent souvent sur les modèles génératifs, cette société a choisi une voie plus discrète mais potentiellement plus structurante : garantir la solidité des résultats.

La valorisation de 1,6 milliard de dollars reflète la conviction que la formalisation à grande échelle peut devenir un avantage concurrentiel décisif. Alors que la plupart des acteurs se battent sur la qualité des réponses générées, Axiom Math construit le terrain sur lequel ces réponses pourront être validées.

Les défis qui restent à relever

Formaliser 7 654 pages représente un exploit, mais ce n’est qu’une partie du corpus mathématique mondial. D’autres domaines restent encore peu couverts. Maintenir et étendre une telle bibliothèque demandera un effort continu. Les agents devront également apprendre à formaliser des résultats nouveaux, et non seulement à traduire des textes existants.

La question de l’adoption se pose aussi. Les mathématiciens et les ingénieurs devront s’habituer à travailler avec ces outils. La courbe d’apprentissage du langage Lean, bien que facilitée par les agents, reste présente. Enfin, la confiance dans les modèles formateurs d’Axiom Math devra être constamment prouvée par des résultats concrets.

Pourquoi cette initiative arrive au bon moment

La multiplication des annonces d’avancées mathématiques par des systèmes d’intelligence artificielle a créé un climat de méfiance justifié. Quand des centaines de manuscrits sont publiés en même temps, la capacité humaine de vérification est rapidement saturée. Les assistants de preuve offrent une solution, mais uniquement s’ils disposent d’une base suffisamment large et cohérente.

En comblant le trou en géométrie algébrique, Axiom Math retire un obstacle majeur. Les futurs travaux dans ce domaine pourront être formalisés plus rapidement. La boucle vertueuse décrite par Terence Tao peut enfin s’enclencher à grande échelle.

Parallèlement, l’explosion du code généré par intelligence artificielle rend la question de la fiabilité plus urgente que jamais. Les failles de sécurité dans des systèmes critiques ne sont plus seulement un risque théorique. Disposer de composants déjà vérifiés formellement peut devenir un standard de sécurité.

Une vision plus large de l’intelligence artificielle

Axiom Math ne se contente pas de résoudre un problème technique. La société propose une philosophie différente de l’intelligence artificielle. Au lieu de produire toujours plus de contenu, elle cherche à produire du contenu dont la solidité peut être prouvée. Cette approche contraste avec la logique purement generative qui domine actuellement le secteur.

Les agents d’Axiom Math ont démontré qu’ils pouvaient collaborer de manière autonome sur une tâche complexe et délicate. Cette capacité d’organisation spontanée, combinée à une spécialisation mathématique, ouvre des perspectives intéressantes pour d’autres domaines scientifiques où la rigueur est essentielle.

La formalisation du Stacks Project n’est donc pas seulement une prouesse technique. C’est un signal. Il est possible de bâtir des systèmes d’intelligence artificielle qui renforcent la fiabilité plutôt que de l’éroder. Dans un monde saturé d’informations approximatives, cette promesse a de quoi séduire.

Ce que les développeurs et les chercheurs peuvent en tirer dès maintenant

Les mathématiciens disposent désormais d’une base formalisée majeure en géométrie algébrique. Ils peuvent s’en servir pour vérifier leurs propres résultats ou pour explorer de nouvelles pistes avec un filet de sécurité. Les développeurs intéressés par la vérification formelle peuvent étudier l’approche d’Axiom Math comme un modèle d’organisation d’agents à grande échelle.

Les entreprises qui développent des logiciels critiques ont intérêt à suivre de près ces avancées. La formalisation n’est plus réservée aux laboratoires de recherche. Elle devient une option concrète pour garantir la solidité de composants essentiels.

Le défi lancé à l’écosystème

En lançant un défi ouvert aux entreprises spécialisées dans le code, Carina Hong place la barre très haut. Formaliser à l’échelle du Stacks Project n’est pas une opération marketing. C’est un projet qui demande une expertise mathématique profonde, des modèles spécialisés et une capacité à orchestrer des milliers d’agents sans perdre la cohérence globale.

Si d’autres acteurs relèvent le défi, le domaine de la formalisation pourrait connaître une accélération significative. Si personne ne suit, Axiom Math se retrouvera en position de quasi-monopole sur une infrastructure potentiellement critique. Dans les deux cas, le signal est clair : la qualité et la vérifiabilité deviennent des enjeux stratégiques.

Perspectives pour les années à venir

À court terme, on peut s’attendre à ce que la bibliothèque formalisée soit enrichie et utilisée par la communauté mathématique. À moyen terme, des applications concrètes en vérification de logiciels devraient apparaître. À plus long terme, la capacité à formaliser automatiquement de nouveaux résultats pourrait transformer la façon dont la science progresse.

La véritable révolution ne réside peut-être pas dans la formalisation d’un corpus existant, aussi impressionnante soit-elle. Elle réside dans la démonstration qu’il est possible de faire collaborer des agents sur une tâche intellectuelle complexe tout en préservant une rigueur absolue. Cette leçon dépasse largement les mathématiques.

Dans un paysage technologique dominé par la génération rapide de contenus, Axiom Math rappelle qu’il existe une autre voie. Une voie où la vitesse n’est pas opposée à la solidité, mais où la solidité devient le prérequis de toute accélération durable. Les 16 millions de lignes de Lean du Stacks Project constituent peut-être le premier étage d’un édifice beaucoup plus vaste.

Les prochaines annonces de la société seront suivies avec attention. Si elle parvient à étendre cette approche à d’autres domaines scientifiques ou à des logiciels industriels, le paysage de l’intelligence artificielle pourrait en être durablement modifié. Pour l’instant, une chose est certaine : les mathématiques disposent désormais d’une fondation formellement vérifiée d’une ampleur inédite. Et ce n’est probablement que le début.

La bataille contre le contenu approximatif généré par intelligence artificielle ne se gagnera pas uniquement en améliorant les modèles. Elle se gagnera aussi en construisant des bases solides sur lesquelles ces modèles pourront s’appuyer. Axiom Math vient de poser une de ces bases. Reste à voir combien d’autres suivront, et à quelle vitesse.