Tech Teardown 042 | Stacks : 7 500 pages en 16 M de lignes Lean

Contexte et phénomène : Une déclaration « la plus grande de l’histoire » avec 94 étoiles

Le 4 novembre 2026, Axiom (axiommath.ai) a publié un blog signé annonçant la réalisation de la version Lean de tout le projet Stacks Project : environ 16 millions de lignes de code (chiffre officiel, car le dépôt est trop volumineux et aucune vérification indépendante des lignes n’a été effectuée), présentant comme « la plus grande bibliothèque mathématique intégrée et réutilisable de l’histoire ». Le dépôt AxiomMath/Stacks utilise la licence Apache-2.0, et la chaîne d’outils est fixée à lean4 v4.34.0-rc2 ; selon des données collectées le 6 novembre 2026, le dépôt a reçu 94 étoiles, avec seulement 66 articles HN et 17 commentaires. La taille de la déclaration et la popularité réservée à sa réponse constituent le premier point d’observation de cette analyse. Pourquoi la publication d’une bibliothèque mathématique mérite-t-elle une analyse technique ? Parce qu’elle pourrait être le plus grand exemple de projet « l’IA écrit du code, les humains définissent les normes, les machines vérifient » à ce jour.

Le projet Stacks Project est lui-même la base de la géométrie algébrique : un ouvrage de référence ouvert, initié en 2005 par le mathématicien de l’Université Columbia Johan de Jong, comptant environ 7500 pages, avec des contributions de plusieurs centaines de mathématiciens au cours de vingt ans. Les principes d’édition sont que chaque théorème est accompagné d’une preuve, les hypothèses sont explicitées, et les dépendances peuvent être remontées jusqu’à quatre caractères de tag. De Jong se compare à « un gardien des bases mathématiques comme celui du noyau Linux ». Une preuve contemporaine de la géométrie algébrique moderne peut nécessiter des connaissances en algèbre commutative, conorme, couches, homothéorie et chaînes de longs théorèmes d’algèbre stack. Lean manquait précisément de cette infrastructure. La motivation d’Axiom est très claire : la vitesse à laquelle l’IA génère des arguments mathématiques dépasse de loin la capacité de la vérification humaine, rendant ainsi la vérification formelle indispensable.

Architecture et principes techniques : mapping des tags, double inspection, audit multi-agent

Le premier mécanisme est la comparaison permanente. Chaque déclaration Lean porte l’attribut @[stacks TAG], renvoyant au tag de quatre caractères du texte original de Stacks Project ; un tag peut correspondre à plusieurs déclarations, et les annotations des attributs indiquent quelles parties sont couvertes lors d’une certaine couverture ; les tags déjà couverts par Mathlib sont enregistrés dans les déclarations de Mathlib via add_to_stacks. Les déclarations indiquent également les numéros d’article de Grothendieck « EGA » et « SGA » correspondant à leurs preuves (par exemple, l’attribut @[ega] porte le numéro d’article IV 7.8.3), avec des annotations distinctives entre quatre catégories : « entier / plus général / partie de la phrase / cas spécial ». Le site web correspondant stacks.axiommath.ai propose une visualisation côte à côte du texte original et du code Lean, ainsi qu’un graphique interactif des dépendances.

Le deuxième niveau est un système de double inspection. Le dépôt est divisé en deux répertoires : StacksCore et StacksFrontier. Core contient le code qui a été examiné manuellement, vérifié par rapport au texte original et qui respecte les normes de nommage, de généralité et de style de Mathlib ; Frontier contient le code écrit par des agents IA, couvrant les parties en croissance la plus rapide et nécessitant le plus de vérification avant d’être intégré à Core. Le README explique clairement : la seule différence entre les deux niveaux est « qui a examiné le code », et tous deux passent également l’inspection du Lean kernel.

Le troisième niveau est l’ingénierie des agents. Axiom a déployé un « cluster d’agents AI coordonnés », qui traduisent en parallèle les déclarations, recherchent les abstractions existantes de Mathlib, construisent des preuves et résolvent les dépendances préalables, en utilisant un système d’agents hiérarchisé et des protocoles de coordination strictes (le blog ne fournit pas les détails des protocoles). La fidélité des déclarations est garantie par trois mécanismes : l’audit multi-agents, le contrôle sémantique croisé sur le texte original, et la contrainte stricte que « chaque lemme défini doit être correctement connecté au théorème dérivé ».

Le quatrième niveau est un circuit de correction guidé par des exemples négatifs. Au cours du processus de formalisation, des dizaines de déclarations dans le texte original de Stacks ont nécessité des corrections partielles : présence de hypothèses manquantes, cas marginaux dans le domaine des caractéristiques positives, déclarations trop larges pour être valides. L’agent est chargé de diagnostiquer les obstacles mathématiques et de construire des exemples négatifs explicites ; lorsque un lemme faux crée un manque dans la preuve d’un théorème profond, il cherche une voie alternative dans la littérature pour reconstruire le théorème principal sous les mêmes hypothèses.

Données clés : 63k modules, zéro sorry, trois axiomes

Les chiffres suivants sont rapportés par l’équipe officielle ou par le repository lui-même, sans vérification par des tiers pour l’instant.

La taille totale est estimée à environ 16 millions de lignes ; le README indique environ 63 000 modules, affirmant que « chaque tag contenant du contenu formel dans le projet Stacks a été formalisé » (c’est la version rapportée par le README), tandis que les exemples, exercices et remarques non formels sont laissés à la communauté pour traitement.

Il y a trois indicateurs de qualité : Lean kernel vérifie chaque preuve ; il n’y a pas de sorry ni de native_decide dans tout le repository ; seuls les axiomes standard propext, Classical.choice et Quot.sound sont utilisés, et toute personne peut vérifier avec l’commande #print axioms.

Le coût de construction est un obstacle réel : l’instruction officielle est lake exe cache get && lake build, ce qui nécessite beaucoup de temps et d’espace mémoire pour la construction complète ; l’équipe officielle prévoit de fournir un service de cache de compilation, mais cela n’a pas encore été mis en œuvre. En d’autres termes, cette bibliothèque de 63k modules n’est pas particulièrement adaptée aux machines individuelles pour l’instant.

Données communautiques : recueillies le 6 novembre, le repository a un score de 94★ ; les articles HN (story 50380979, publié le 5 novembre 2026) ont un score de 66▲ et 17 commentaires. Le nombre total de commentaires n’est pas élevé, mais leur qualité est remarquable : il y a des jugements positifs sur les approches formelles, ainsi que des questions directes sur la philosophie de la vérification. En comparaison, la même organisation a publié en 2026-10-27 une formalisation de la classification des groupes uniques (CFSG), et Axiom a distingué les deux : CFSG se concentre sur un théorème de point de repère unique et est moins organisé ; Stacks est une bibliothèque de base, dont la valeur réside dans les milliers de définitions, constructions et lemmes interdépendants qui sont réutilisés à plusieurs reprises, tandis que les défis d’ingénierie sont essentiellement différents.

Impact et signification : transformer « la fidélité des déclarations » en une propriété auditable

Le premier point est l’utilisabilité. Ce n’est pas un monument, mais une base : les mathématiciens et les agents d’IA peuvent importer les Stack et appeler directement aux bases de la géométrie algébrique, en utilisant les commandes #stacks_tags et #stackstags! pour lister toutes les déclarations portant des tags. Ce qui est ajouté, c’est le vide de la géométrie algébrique moderne dans l’écosystème Lean ; par la suite, la formalisation de ce domaine peut s’y appuyer sans avoir besoin d’être traduite à partir de zéro. Cela est particulièrement vrai pour les agents : le board de tâches divise « quels exemples n’ont pas encore été formalisés » en tâches disponibles, et le README invite clairement la critique communautaire du code Frontier pour être intégré au Core, ce qui équivaut à préparer un chemin pour les contributions mathématiques assistées par l’IA.

Le deuxième point est le signal de formalisation qui nourrit les mathématiques. Des dizaines de déclarations originales ont été identifiées comme nécessitant des corrections, et les agents ont construit des exemples anti-explicit, montrant que la formalisation à grande échelle n’est pas seulement une traduction, mais aussi un examen automatique du texte original. HN a souligné que le projet Stack itself ressemblait à « Lean écrit en langue naturelle » : chaque théorème est accompagné d’une preuve, les hypothèses sont explicitées, et les dépendances peuvent être révélées, donc une formalisation de haute qualité n’est pas surprenante ; un autre commentateur a dit que CFSG s’attendait à ce que quelqu’un tente de modifier Stack après sa publication.

Le troisième point est l’inspiration méthodologique pour l’ingénierie d’IA en dehors des mathématiques (c’est mon jugement). Lorsque l’IA génère des codes en masse, le point le plus fragile n’est pas la validité de la preuve, mais la fidélité des déclarations à l’intention originale : le kernel peut vérifier la première, mais pas « si la théorie est correctement traduite ». Le trio offert par Axiom – l’audit multi-agents, le contrôle sémantique croisé, les contraintes rigides de liaison avec le downstream – est essentiellement rendre « la fidélité des déclarations prioritaire à la justesse de la preuve » une axiologie d’ingénierie. Cette approche peut être directement transférée à tout scénario de audit à grande échelle où l’IA traduit pour générer du code.

Controverses et risques : rejet en amont, critiques de texte et différence de performance au démarrage

Le conflit le plus aigu se situe en amont. Le 21 octobre 2026, de Jong a demandé dans un annonce en amont de ne pas soumettre directement des commentaires ou des PR générés par l’IA dans le répertoire du projet Stack (selon les propos rapportés par le blog Axiom). Axiom a exprimé son respect pour cette limite : la formalisation, les exemples anti-explicit, les corrections restent tous dans son propre répertoire, tandis que l’amont est toujours géré par de Jong et la communauté, disponible pour les mathématiciens à examiner et utiliser à leur propre rythme. HN a souligné le point sensible ici : le dernier article du blog original Stack le 21-10 portait justement le titre « No AI for now », et le commentateur avait été déçu par les progrès de la mathématique assistée par l’IA. En d’autres termes, ces 16 millions de lignes de code n’ont actuellement qu’une identité de projet indépendant, sans l’approbation en amont.

La deuxième controverse concerne le texte de l’article. Plusieurs commentateurs sur HN ont critiqué la publication du blog comme une exemple typique de “slop AI” : des métaphores comme “Ce jalon commence par” rendent le résultat moins fiable. Les commentaires réfutatoires sont également directs : certains ont souligné que Axiom a reçu un financement important (ce commentateur affirme qu’il n’a pas été vérifié indépendamment), et que le blog publie des preuves Lean construites par l’IA, avec l’IA écrite dans le nom de domaine. Pourquoi alors critiquer le style d’AI utilisé dans le texte ? Mon avis : les critiques du texte ne touchent pas à la substance technique, mais elles abordent un vrai problème : le blog ne dispose pas de documents open-source sur le protocole de coordination des “clusters d’agents”, et plus ce mécanisme est opaque, plus le style du texte peut être exagéré (c’est mon jugement).

Le troisième point concerne la différence entre un lancement froid et un lancement chaud. L’annonce de “la plus grande bibliothèque mathématique formalisée de l’histoire” ne correspond pas à l’intérêt suscité par 94★ et 17 commentaires sur HN. Les raisons objectives sont : le coût de construction complète est élevé, les services de cache ne sont pas encore lancés, et le public de la géométrie algébrique est déjà restreint. Le sujet a même dépassé les frontières de la géométrie : un commentateur a corrigé un débat qui s’était éloigné du sujet, indiquant que ce Stack était une “stack” en géométrie algébrique, et non une stack technique. Cette interprétation erronée montre que l’attention suscitée par la publication a dépassé les frontières professionnelles. Mais HN a également soulevé des questions philosophiques : comment valider la fidélité de la hypothèse ? La section d’audit des agents du blog est en fait la réponse, mais le commentateur qui a posé la question n’a pas lu cette information. Un autre commentaire est encore plus fondamental : même si toute preuve est correcte, les obstacles dans les mathématiques à l’ère de l’IA restent l’interprétation humaine ; ceux qui ne réalisent pas de problèmes ou ne lisent pas des preuves ne comprendront pas en raison de la taille croissante de la bibliothèque.

Conclusion et perspectives : seules les bibliothèques que l’on peut importer sont véritablement des monuments

La phrase clé est : Axiom a traduit un ouvrage de 7500 pages sur la géométrie algébrique en environ 16 millions de lignes de code Lean (comme l’a déclaré l’équipe officielle), utilisant trois axiomes standards, zéro “sorry”, un contrôle complet du kernel et un système de révision à deux niveaux Core/Frontier. Cependant, la frontière entre “refus des contributions IA” reste non résolue.

L’entrée pour participer est simple : importer les Stacks directement, rechercher avec le tag #stacks_tags ; réclamer des tâches sur le board de stacks.axiommath.ai/contributing, et utiliser la mention “claim” sur les issues GitHub pour éviter les collisions. Vérifier le code de Frontier et le promouvoir dans Core est la manière de contribuer la plus nécessaire actuellement. Trois choses importantes à surveiller : si le service de cache de compilation sera lancé (cela détermine si 63k modules peuvent être utilisés par des développeurs ordinaires), si Axiom rendra publiques les détails du protocole de coordination des agents (cela détermine si l’audit multi-agent peut être reproduit), et si la politique de de Jong change (cela détermine si cette bibliothèque peut être intégrée dans un projet indépendant).

Pour les développeurs ordinaires, même s’ils ne se consacrent pas à la géométrie algébrique, ce repository offre un modèle à suivre : comment concevoir une échelle de révision pour des bibliothèques de code de grande taille générées par l’IA, et comment faire en sorte que “la fidélité aux besoins originaux” devienne une contrainte vérifiable. Ma conclusion est simple : ce qui est intéressant avec Stacks n’est pas le chiffre de 16 millions de lignes, mais plutôt le fait qu’il divise la question “La mathématique écrite par l’IA est-elle fiable ?” en deux questions distinctes : la validité est assurée par le kernel, tandis que la fidélité est vérifiée par l’audit comparatif. Le premier fournit une garantie ferme, tandis que le second propose un plan de développement mais sans publication au niveau du protocole. C’est là son plus grand défi actuel.

Sources de référence

• Blog officiel d’Axiom (axiommath.ai, publié le 04-11-2026, signature Axiom ; 16 millions de lignes, cluster d’agents, corrections des contre-exemples sont tous conformes aux déclarations officielles ; texte intégral stocké localement dans stacks.txt)
• Repos : github.com/AxiomMath/Stacks (94★ / Apache-2.0 / lean4 v4.34.0-rc2 / branche main, snapshot récupéré le 06-11-2026 ; README de 59 lignes contient le texte intégral ; le repos étant trop grand, il n’a pas été cloné, le nombre de lignes n’a pas été mesuré)
• Article sur HN : story 50380979 (66▲ / 17 commentaires, publié le 05-11-2026, snapshot du 06-11-2026 ; la pile de commentaires hn-stacks-full.json contient 11 entrées, le texte principal a été transposé sans citation directe)
• Contexte upstream de Stacks Project et annonce de de Jong du 21-10-2026 : tous sont conformes aux déclarations reprises sur le blog officiel d’Axiom

Signature : Yongliang