AxiomMath annonce la vérification formelle du projet Stacks
AxiomMath a annoncé la vérification formelle du projet Stacks mercredi, marquant une étape significative pour ses opérations dans le domaine mathématique. Le projet Stacks, connu pour son corpus complet de mathématiques, s’étend sur environ 7 654 pages et a été décrit par des mathématiciens comme Peter Woit de Columbia comme sans précédent en termes d’envergure. AxiomMath, une startup valorisée à 1,6 milliard de dollars, vise à créer un cadre fondamental solide sur lequel des agents d’IA peuvent établir des logiciels fiables et contribuer à l’avancement scientifique, rapporte 24brussels.
Initié en 2005 par le mathématicien Johan de Jong, le projet Stacks fonctionne comme une référence open-source, avec des contributions d’un large éventail de mathématiciens au fil des années. Cette initiative englobe des résultats allant de l’algèbre de premier cycle à des concepts avancés en algèbre, géométrie et théorie des nombres.
Les actifs technologiques d’AxiomMath comprennent une suite d’agents AI conçus pour transformer la vaste bibliothèque de Stacks en environ 16 millions de lignes de code validées par ordinateur. Ce processus de formalisation garantit que la structure fondamentale des mathématiques est fiable, les preuves étant réécrites dans un langage de programmation nommé Lean, qui est méticuleusement vérifié ligne par ligne par un assistant de preuve.
La vérification formelle est un principe également utilisé en ingénierie pour valider les conceptions de puces et garantir l’intégrité des logiciels, comme en témoignent diverses applications de recherche en France ayant tiré parti de cette technique pour détecter les défauts opérationnels.
Le réseau complexe de théorèmes interconnectés du projet Stacks nécessite la préservation rigoureuse des relations durant le processus de vérification, entraînant des défis pour Axiom.Math dans le maintien de la cohérence à travers le code extensif en Lean.
La PDG d’AxiomMath, Carina Hong, a exprimé son inquiétude concernant la nature délicate des grandes structures mathématiques. « Les choses qui sont grandes et délicates dans la vie ne vont tout simplement pas ensemble », a déclaré Hong, soulignant l’importance de définitions cohérentes et non contradictoires au sein des constructions mathématiques.
Ayant précédemment abandonné un programme de doctorat à Stanford, Hong a fondé AxiomMath en mars 2025, sécurisant 200 millions de dollars lors d’une levée de fonds de série A dirigée par Menlo Ventures.
Pour atteindre cet ambitieux projet, AxiomMath a adopté une structure de travail collaborative pour ses agents, leur permettant d’identifier et de poursuivre diverses tâches de manière autonome et en parallèle. « Avec Stacks, nous avons imposé une hiérarchie… [mais] ce n’était pas, en fait, une hiérarchie complète dictant ce que chaque agent faisait », a déclaré Ashvin Swaminathan, membre de l’équipe technique d’Axiom.
AxiomMath a également développé des modèles propriétaires formés pour interpréter les mathématiques, divergeant des méthodologies typiques d’autres startups de vérification. Au départ, l’équipe s’est appuyée sur des experts Lean en interne pour les orienter, permettant progressivement aux agents de peaufiner leur compréhension de manière autonome.
La vérification du projet Stacks comble une lacune critique dans les mathématiques formelles, en particulier dans le domaine de la géométrie algébrique. Swaminathan a souligné qu’il y a peu encore, les chercheurs avaient des ressources limitées pour étayer leurs nouvelles investigations dans ce domaine.
Axiom vise à établir chaque résultat vérifié comme un élément fondamental pour les preuves futures, facilitant la construction des mathématiques sur des résultats établis plutôt que de repartir de zéro. Terence Tao, un mathématicien de renom, a fait remarquer qu’une formalisation accrue conduit à encore plus de preuves formelles.
Au-delà de la communauté mathématique, AxiomMath reconnaît l’urgence pour les développeurs de s’assurer que leurs logiciels sont exempts d’erreurs alors que les systèmes d’IA contribuent de plus en plus à la génération de code.
Axiom prévoit que les logiciels de demain nécessiteront une base vérifiée similaire à celle des Stacks. « Nous croyons que les mathématiques sont le domaine où vous commencez à construire ces choses, et que c’est une compétence transférable », a déclaré Swaminathan.
Hong envisage l’approche de tâche parallèle des agents d’Axiom comme un précurseur des futurs développements de l’IA. « Vous voulez que [les agents] aient une bibliothèque réutilisable sur laquelle se baser et continuer à faire avancer la frontière », a-t-elle noté, défiant les entreprises de codage de s’engager dans les efforts de formalisation à grande échelle entrepris par Axiom.
