Axiom Math vérifie le Stacks Project pour contrer le « slop » de l'IA

Le principe de la vérification

Les mathématiciens réécrivent une preuve sous forme de code dans le langage Lean, puis un assistant de preuve la contrôle ligne par ligne. Les ingénieurs recourent à la même idée, la vérification formelle, pour valider des conceptions de puces, et des chercheurs en France l'ont utilisée pour détecter des bogues dans un logiciel de calcul des allocations familiales.

Stacks était un défi, car ses théorèmes et définitions s'appuient les uns sur les autres, comme dans un arbre généalogique. Le mathématicien de Columbia Johan de Jong a lancé ce projet libre en 2005. Il couvre de l'algèbre de niveau universitaire à la géométrie algébrique et à la théorie des nombres. « Ce qui est grand et ce qui est délicat ne vont pas ensemble », a déclaré la directrice générale Carina Hong.

Axiom a donné à ses agents une hiérarchie souple et les a laissés travailler en parallèle, en choisissant eux-mêmes leurs tâches. L'entreprise a aussi entraîné ses propres modèles de mathématiques. Selon Ashvin Swaminathan, il existait un « immense trou noir » en géométrie algébrique dans les mathématiques formalisées, sur lequel les chercheurs utilisant Lean peuvent désormais s'appuyer.

Au-delà des mathématiques

Axiom estime que chaque résultat vérifié devient une brique. Terence Tao résume : « Plus on a de preuves formalisées, plus on peut en produire. » Les développeurs sont aussi visés, car garantir un code sans bogues ni failles devient plus difficile à mesure que les agents d'IA écrivent du logiciel.

Carina Hong, 25 ans, a abandonné un doctorat de mathématiques à Stanford et fondé Axiom en mars 2025. En mars, la société a levé 200 millions de dollars en série A, menée par Menlo Ventures. Elle lance un défi ouvert aux entreprises de programmation : travailler sur la formalisation à cette échelle.