# Axiom formalise le Stacks Project en Lean, avec vérification automatique

> Selon Axiom, sa formalisation de 16 millions de lignes rend une référence majeure en géométrie algébrique réutilisable dans des preuves vérifiées par Lean.

Oossa · 2026-11-05 · https://oossa.com/fr/axiom-turns-the-stacks-project-into-machine-checked-lean-code

Axiom Math a publié une version vérifiée par ordinateur du Stacks Project, une importante référence libre en géométrie algébrique. Cette formalisation traduit les mathématiques du projet en quelque 16 millions de lignes de code Lean, vérifiées étape par étape par un programme. Axiom affirme que les chercheurs et les agents d’IA pourront utiliser ces résultats comme une bibliothèque interconnectée pour élaborer de nouvelles preuves formelles.

Les sources indiquent des nombres de pages légèrement différents : TechCrunch parle d’environ 7 654 pages, tandis qu’Axiom décrit le projet comme comptant quelque 7 500 pages. Cette référence a été lancée en 2005 par le mathématicien de Columbia Johan de Jong, puis enrichie par des mathématiciens pendant deux décennies. Le travail d’Axiom formalise ces recherches existantes ; cela ne signifie pas que les agents d’IA ont découvert de manière indépendante les mathématiques sous-jacentes.

## Pourquoi une bibliothèque interconnectée est-elle utile ?

L’intérêt d’une bibliothèque de preuves ne tient pas seulement à la vérification de chacun de ses théorèmes : les preuves ultérieures peuvent aussi réutiliser ces résultats et leurs dépendances. Axiom indique avoir conservé les balises permanentes du Stacks Project, qui relient les déclarations Lean aux passages correspondants du texte original. Son site permet également de consulter le texte à côté du code et d’explorer les liens de dépendance entre les résultats.

C’est particulièrement important en géométrie algébrique, où une preuve peut s’appuyer sur une longue chaîne d’idées issues de domaines comme l’algèbre commutative, les schémas, les faisceaux et la cohomologie. Axiom affirme qu’avant cette publication, les chercheurs disposaient de beaucoup moins d’outils Lean pour formaliser la géométrie algébrique moderne. La bibliothèque de l’entreprise leur fournit une base de départ, au lieu de les obliger à formaliser à nouveau ces fondements pour chaque projet.

## Une base pour les preuves et les logiciels de demain

Axiom indique que ses agents ont travaillé en parallèle pour traduire, démontrer et intégrer des milliers de théorèmes. Selon TechCrunch, l’entreprise leur a donné un cadre souple afin qu’ils puissent repérer les tâches à accomplir ; Axiom a également entraîné ses propres modèles spécialisés en mathématiques. L’entreprise présente la bibliothèque achevée comme la plus grande bibliothèque intégrée et réutilisable de mathématiques formalisées. Il s’agit de la caractérisation que fait Axiom de cette publication.

Ce type de vérification est également utilisé dans des domaines comme la conception de puces et la vérification de logiciels. Selon Axiom, des fondements vérifiés et réutilisables pourraient aider les agents d’IA à créer des systèmes plus fiables à mesure qu’ils écrivent davantage de code. Mais cette publication vérifie le Stacks Project formalisé, et non chaque nouvelle affirmation mathématique ou chaque logiciel qu’un système d’IA pourrait produire.

## Les faits

- Axiom a daté sa publication du 4 novembre 2026.
- La formalisation en Lean comprend environ 16 millions de lignes de code.
- Le Stacks Project a été lancé par Johan de Jong en 2005 et s’est étoffé grâce aux contributions de mathématiciens.
- Selon TechCrunch, Axiom a levé 200 millions de dollars lors d’un tour de table de série A mené par Menlo Ventures en mars 2026.

## Pourquoi c'est important

Pour les mathématiciens qui travaillent en géométrie algébrique, cette bibliothèque met à leur disposition des résultats vérifiés qu’ils peuvent réutiliser, plutôt que de reconstruire les mêmes fondements en Lean. Elle confirme la formalisation de cette référence, mais ne garantit pas la fiabilité des futures preuves ou du code générés par l’IA sans vérification.

## Sources et références

1. [Axiom Math wants to keep AI slop out of mathematics](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/) – TechCrunch, 2026-11-05
2. [Axiom](https://axiommath.ai/research/the-stacks-project-formalized/?utm_source=openai) – Axiom

Dernière mise à jour: 2026-11-05