Axiom publie une formalisation en Lean de tout le Stacks Project, environ 16 millions de lignes produites par des essaims d'agents IA
La référence de géométrie algébrique d'environ 7 500 pages devient une bibliothèque unique vérifiée par machine ; des mathématiciens extérieurs n'ont pas encore jugé la fidélité des énoncés.
Pourquoi c’est important
La géométrie algébrique moderne n'avait guère d'infrastructure Lean, car une seule preuve peut reposer sur de longues chaînes de résultats d'algèbre commutative, de schémas, de faisceaux et de cohomologie. Axiom indique que sa bibliothèque conserve les étiquettes permanentes du Stacks Project, si bien que humains et agents IA peuvent importer ses définitions et théorèmes dans de nouvelles preuves. Elle suit la formalisation en Lean de la classification des groupes simples finis publiée par Axiom le 27 octobre 2026. Reste à voir si les mathématiciens qui comparent les énoncés au texte d'origine les jugent fidèles, et si la bibliothèque est adoptée aux côtés de Mathlib.
Faits clés
- Stacks Project : environ 7 500 pages
- Environ 16 millions de lignes de code Lean
- Réalisé par des essaims coordonnés d'agents IA
- Lancé par Johan de Jong, de l'université Columbia, en 2005
- Consultable sur stacks.axiommath.ai
- Fait suite à la formalisation CFSG d'Axiom du 27 octobre 2026