On a l’impression que l’intelligence artificielle résout presque chaque semaine un nouveau problème mathématique. Le mois dernier, seule OpenAI a publié 719 manuscrits affirmant avoir résolu certains des problèmes les plus difficiles du domaine. Même la vérification par ordinateur peut comporter des erreurs. Après des années de contenu de mauvaise qualité généré par l’IA, on ne peut s’empêcher de se demander si les mathématiques seront le prochain domaine touché.
AxiomMath peut éviter ce destin non en ralentissant, mais en établissant une base plus solide. Cette start-up évaluée à 1,6 milliard de dollars souhaite créer une couche de base vérifiée sur laquelle les agents IA pourront s'appuyer pour écrire des logiciels, puis effectuer des recherches scientifiques.
Mercredi, l'entreprise a annoncé avoir officiellement validé le projet Stacks, l'une des plus grandes réalisations mathématiques jamais écrites par des humains. Les mathématiciens évaluent généralement Stacks très haut. Le mathématicien de l'Université Columbia Peter Woit l'a qualifié de « presque rien d'autre ne peut lui être comparé » et a comparé le projet aux « célèbres volumes de Bourbaki » — cette série d'ouvrages qui ont reconstruit les fondements des mathématiques au XXe siècle.
Le collègue colombien de Woit, Johan de Jong, a lancé le projet Stacks en 2005 comme une référence open source. Depuis, des mathématiciens y contribuent continuellement, en étendant les contenus depuis l'algèbre au niveau universitaire jusqu'aux idées les plus avancées en algèbre, géométrie et théorie des nombres.
Le groupe d'agents IA de l'entreprise a traduit cette base de données d'environ 7 654 pages en environ 16 millions de lignes de code vérifiables par ordinateur.
L'objectif des mathématiques formelles est de garantir que leur structure sous-jacente est fiable. Les mathématiciens réécrivent les preuves sous forme de code à l'aide d'un langage de programmation appelé Lean, puis un programme appelé assistant de preuve vérifie ces codes ligne par ligne. Si la preuve est validée, les mathématiciens peuvent être certains qu'elle est logiquement correcte.
Les ingénieurs utilisent également cette même approche, appelée vérification formelle, pour vérifier la faisabilité de la conception de puces ; des chercheurs français l'ont utilisée pour découvrir une faille dans un logiciel de calcul des allocations familiales.
Pour un projet comme Stacks Project, vérifier les théorèmes un par un n'est qu'une partie du travail. Les théorèmes et définitions dans Stacks sont interconnectés, chacun s'appuyant sur les précédents. Comme un arbre généalogique, de nombreux résultats dans Stacks peuvent être remontés à des résultats antérieurs.
Cette interdépendance a rendu Axiom incertain au départ quant à la faisabilité du projet. L'équipe devait maintenir chaque connexion intacte dans environ 16 millions de lignes de code Lean.
Carina Hong, PDG d'Axiom, a déclaré à TechCrunch : « La taille et la finesse ne sont généralement pas compatibles dans la réalité. [Stacks] est un ensemble de résultats mathématiques qui constituent les fondements mathématiques. Vous souhaitez que les [théorèmes] soient cohérents entre eux, et non contradictoires comme des paradoxes. Vous souhaitez également que ces définitions ne se contredisent pas entre elles. »
Ce PDG de 25 ans a abandonné son doctorat en mathématiques à Stanford et a fondé cette entreprise en mars 2025. En mars de cette année, Axiom a levé 200 millions de dollars lors d'un tour de financement Série A dirigé par Menlo Ventures.
Hong a déclaré : « Nous n'étions pas certains que le vibe coding puisse préserver l'esthétique de Stacks. »
Pour mener à bien ce projet, l'équipe a défini une structure flexible pour les agents et les a fait s'exécuter en parallèle. « Pour Stacks, nous avons établi une hiérarchie... mais pas une hiérarchie qui définit exactement ce que chaque agent doit faire. Les agents trouvent eux-mêmes les tâches et identifient celles qui peuvent être traitées en parallèle », explique Ashvin Swaminathan, membre de l'équipe technique d'Axiom.
Axiom a également formé ses propres modèles pour les rendre excellents en mathématiques. Hong affirme que cette approche n'est pas adoptée par la plupart des autres startups de vérification. Au départ, l'équipe s'appuyait sur un expert interne en Lean pour enseigner aux agents des critères de jugement similaires à ceux des humains. Avec le temps, selon Hong, ces agents ont appris eux-mêmes ce jugement.
Ce résultat remplit l'un des plus grands trous de la mathématique formalisée. « Lorsque vous examinez le contenu mathématique déjà formalisé, vous constatez qu'il y a un énorme trou noir. Et ce trou noir couvre la géométrie algébrique », dit Swaminathan.
Swaminathan a déclaré qu'auparavant, les chercheurs souhaitant utiliser Lean pour vérifier de nouveaux travaux en géométrie algébrique avaient très peu de bases prêtes à l'emploi. « Maintenant, elles ont cela. »
Axiom estime que chaque résultat vérifié devient un bloc de construction sur lequel des preuves futures peuvent s'appuyer, sans avoir à recommencer depuis le début. Le mathématicien de l'UCLA et lauréat de la médaille Fields Terence Tao a résumé cela de manière plus concise : « Plus vous avez de preuves formalisées, plus vous pouvez en produire. »
Le public cible d'Axiom ne se limite pas aux mathématiciens. Les développeurs s'efforcent depuis longtemps de garantir que leur code est exempt de vulnérabilités et de failles de sécurité. Avec les agents IA qui écrivent de plus en plus de logiciels, ce problème ne fera que s'aggraver.
Axiom betting, the software of the future needs to be built on proven foundations, just like Stacks today.
Swaminathan dit : « Nous pensons que les mathématiques sont le domaine à partir duquel vous commencez à construire ces choses, et c'est une compétence transférable. Les agents peuvent lire notre code, le comprendre et y construire de nouvelles infrastructures. Ce que nous avons formalisé avec Lean devient désormais le fondement de base sur lequel les agents peuvent s'appuyer. »
La manière dont Axiom construit des agents pour Stacks — travailler en parallèle, choisir ses propres tâches — est exactement ce que Hong anticipe comme la façon dont de nombreux travaux par IA seront effectués à l'avenir. Elle estime que les agents IA ont besoin d'une base de connaissances bien structurée et réutilisable pour éviter de produire du contenu de mauvaise qualité.
Hong dit : « Vous voulez que [l'agent] dispose d'une base réutilisable sur laquelle il peut continuer à construire et repousser les limites. Si vous commencez en y intégrant des choix d'ingénierie médiocres et du mauvais code, il sera difficile d'étendre cette frontière. »
Hong est très confiante en cette méthode et a même lancé un défi public. Elle a déclaré : « Je défie publiquement toutes les entreprises de programmation à réaliser ce type de travail formel à cette échelle. »