La startup Axiom Math dit avoir formalisé en Lean le Stacks Project, vaste bibliothèque de mathématiques, à l’aide d’agents d’IA. Elle y voit un socle réutilisable pour des agents et des développeurs, et défie les entreprises de codage de s’attaquer à la formalisation à cette échelle.
Axiom cible les agents et met les codeurs au défi de formaliser à grande échelle
Carina Hong lance un défi public aux entreprises de codage : travailler sur la formalisation à l’échelle atteinte par Axiom. Elle anticipe que la façon dont les agents ont bâti Stacks, en parallèle et en choisissant leurs tâches, deviendra courante dans les travaux d’IA à venir. Selon elle, ces agents auront besoin d’un corpus réutilisable et bien construit pour éviter le désordre, et de mauvais choix d’ingénierie initiaux brident la progression. Le constat de longue date d’un code difficile à assainir, aggravé par la production croissante de code par des agents d’IA, cadre cette ambition. Axiom parie que le logiciel du futur reposera sur des fondations vérifiées, et Ashvin Swaminathan affirme que leur formalisation Lean sert désormais de substrat que des agents peuvent lire, comprendre et étendre.
Un corpus géant formalisé et un trou en géométrie algébrique comblé
Mercredi, Axiom Math a annoncé la vérification formelle du Stacks Project, en traduisant environ 7 654 pages en quelque 16 millions de lignes de code vérifié. Le Stacks Project est présenté comme l’un des plus grands corpus mathématiques écrits par des humains, et Peter Woit le rapproche des livres de Bourbaki. Ashvin Swaminathan estime que ce travail comble un manque majeur de la formalisation, qui concernait la géométrie algébrique, offrant désormais une base à ceux qui souhaitent vérifier de nouveaux résultats dans ce domaine avec Lean. Terence Tao résume l’enjeu : plus il existe de preuves formalisées, plus il devient possible d’en produire. Axiom soutient enfin que chaque résultat vérifié agit comme un élément de base pour des preuves futures, évitant de repartir de zéro.
Vous voulez les meilleurs outils IA avant les autres ?
On teste et on décrypte les nouveaux outils IA chaque soir, en 5 min. Gratuit.
Inclus dès l'inscription : notre sélection des meilleurs guides & comparatifs IA.
Choisissez votre rythme
Gratuit · Pas de spam · Désabonnement en 1 clic
Agents en parallèle, hiérarchie lâche et modèles maison pour le Lean
Pour mener à bien la formalisation, Axiom a structuré lâchement une flotte d’agents qui se sont auto-attribué des tâches parallélisables, sous une hiérarchie partielle. L’entreprise dit avoir douté au départ de la faisabilité, du fait des interconnexions d’énoncés et de définitions, mais affirme avoir conservé ces liens à travers environ 16 millions de lignes de Lean. Le procédé s’appuie sur la réécriture des preuves en Lean et leur vérification ligne par ligne par un assistant de preuve, une étape rendue plus délicate par la dépendance réciproque des résultats. Axiom a en outre entraîné ses propres modèles pour la compétence mathématique, une option que Carina Hong juge peu courante chez ses pairs, et s’est d’abord appuyée sur un expert Lean interne pour transmettre un sens humain du « goût » aux agents, qui aurait mûri avec le temps.
Ambitions, profil de la fondatrice et moyens financiers d’Axiom
Axiom Math est valorisée à 1,6 milliard de dollars. Carina Hong, qui dirige l’entreprise et est âgée de 25 ans, a interrompu un doctorat en mathématiques à Stanford avant de créer la société en mars 2025. Au mois de mars, la société a obtenu 200 millions de dollars à l’occasion d’une levée de fonds de série A menée par Menlo Ventures. L’objectif affiché consiste à prévenir les erreurs en mathématiques grâce à des fondations solides, et à élaborer une base vérifiée pour permettre aux agents d’IA de rédiger des logiciels et, à terme, d’exercer dans le domaine scientifique.
Vérification formelle, entre usages industriels et contexte d’IA foisonnante
La vérification formelle n’est pas cantonnée aux mathématiques : elle sert à valider des conceptions de puces et a permis en France de déceler des bogues dans des logiciels de calcul de prestations familiales. Ce travail intervient dans un contexte où OpenAI a publié le mois dernier 719 manuscrits revendiquant des solutions à des problèmes ardus, alors qu’il est estimé que l’IA produit sans cesse de nouveaux « résultats » et que même des vérifications informatiques peuvent échouer. Le Stacks Project, lancé en 2005 par Johan de Jong et enrichi depuis par la communauté sur de larges pans des mathématiques, devient ici un terrain d’application. Carina Hong insiste sur la nécessité de cohérence interne des théorèmes et définitions et admet avoir douté que certaines approches, comme le « codage par ambiance », puissent préserver la beauté de Stacks.
