Une ambition audacieuse : formaliser le Stacks Project
Le Stacks Project, vaste recueil de plus de 7 600 pages couvrant l’algèbre, la géométrie et la théorie des nombres, est depuis 2005 une référence open-source pour les mathématiciens. Axiom Math, startup évaluée à 1,6 milliard de dollars, a annoncé avoir converti l’intégralité de ce corpus en environ 16 millions de lignes de code vérifié par le système Lean, un assistant de preuve capable de valider chaque raisonnement ligne par ligne.
Pourquoi la formalisation est cruciale
Les récentes flambées de « slop » généré par l’IA – des prétendues solutions à des problèmes célèbres qui s’avèrent erronées – ont mis en lumière les limites des vérifications automatiques classiques. En traduisant les démonstrations en code Lean, Axiom crée une base solide où chaque théorème repose sur des définitions cohérentes et non contradictoires. Cette approche rappelle la vérification formelle utilisée en ingénierie pour garantir le bon fonctionnement des puces électroniques ou la fiabilité de logiciels publics.
Le défi technique et organisationnel
Transformer un ouvrage aussi interconnecté que le Stacks Project n’est pas une simple tâche de transcription. Les 16 millions de lignes de code doivent conserver les dépendances entre les théorèmes, à l’image d’un arbre généalogique où chaque branche puise ses racines dans les précédentes. L’équipe d’Axiom a donc laissé ses agents d’IA travailler en parallèle, tout en imposant une hiérarchie souple qui leur permettait de choisir leurs propres sous-tâches sans perdre la cohérence globale.
Un leadership atypique
Carina Hong, la PDG de 25 ans qui a abandonné son doctorat en mathématiques à Stanford, dirige la société depuis sa création en mars…2025. Après un tour de table de 200 millions de dollars mené par Menlo Ventures, elle mise sur des modèles internes spécialement entraînés à la rigueur mathématique, une stratégie que peu de concurrents adoptent. Selon Hong, les agents ont progressivement développé « un goût humain » pour la précision, grâce à l’encadrement initial d’experts Lean.
Implications pour l’avenir de l’IA en mathématiques
En comblant le « trou noir » qui sépare les mathématiques formalisées du reste du savoir, Axiom Math ouvre la voie à des systèmes d’IA capables de s’appuyer sur des bases certifiées pour générer du code, proposer des conjectures ou même conduire des expériences scientifiques. Si le projet réussit à rester à l’épreuve du temps, il pourrait devenir le socle sur lequel les futures générations d’assistants intelligents bâtiront leurs découvertes, évitant ainsi les erreurs coûteuses qui ont récemment entaché le domaine.
Source: https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/