Le Stacks Project formalisé en Lean : Axiom publie la plus grande bibliothèque de mathématiques formalisées

Axiom publie sa formalisation en Lean de l'ensemble du Stacks Project, référence open source d'environ 7 500 pages sur les fondations de la géométrie algébrique moderne. La bibliothèque compte quelque 16 millions de lignes de code et se présente comme la plus grande bibliothèque intégrée et réutilisable de mathématiques formalisées. Chaque déclaration Lean est reliée par des tags Stacks permanents au texte canonique. Axiom indique avoir déployé des essaims coordonnés d'agents IA pour traduire, prouver et intégrer des milliers de théorèmes en parallèle.