Faire travailler l’IA sur une bibliothèque de maths sans perdre le sens des théorèmes

Axiom publie une traduction du Stacks Project en Lean, pour réutiliser des preuves contrôlées par ordinateur. La relecture humaine reste un chantier.

Seize millions de lignes de code pour transformer une référence de géométrie algébrique en une bibliothèque de preuves utilisables par ordinateur. Le volume annoncé par Axiom donne la mesure de son projet : traduire les définitions et les résultats du Stacks Project dans Lean, un langage conçu pour écrire et contrôler des raisonnements mathématiques. La publication associe le travail de spécialistes humains et celui d’agents d’IA.

Le dépôt public organise cette traduction en deux ensembles. Le premier rassemble le code relu par des personnes, le second accueille celui des agents qui attend encore cette revue. Les responsables affirment que les preuves passent le contrôle logique de Lean dans les deux cas. Cette distinction est centrale : vérifier un raisonnement formel et vérifier qu’il traduit fidèlement le texte mathématique sont deux travaux différents. Des résultats que l’on peut retrouver et réutiliser

Le Stacks Project original est un ouvrage collectif de référence en géométrie algébrique. Lors de la consultation, son site comptait 7 654 pages et 21 446 éléments identifiés par un tag, répartis dans 116 chapitres. Le contenu s’adresse aux étudiants avancés et aux chercheurs, avec des développements en algèbre commutative et sur les fondements nécessaires à l’étude des espaces géométriques concernés.

Un résultat mathématique utilise souvent des définitions et des propositions établies ailleurs. La difficulté d’une traduction de cette ampleur est donc de préserver les liens entre les éléments, afin qu’une preuve puisse employer ceux dont elle dépend. Le travail publié est construit sur Mathlib, la bibliothèque mathématique de Lean, dont il reprend aussi des résultats déjà disponibles.

Chaque élément du Stacks Project possède un identifiant permanent de quatre caractères. La traduction conserve ces repères pour relier le texte d’origine aux déclarations correspondantes dans le code. Sur le site de consultation, le lecteur peut retrouver un résultat, examiner ses dépendances et accéder à sa formalisation. Lorsqu’un même résultat nécessite plusieurs déclarations Lean, celles-ci restent associées à son identifiant.

Cette organisation donne aux chercheurs et aux systèmes de preuve une base dans laquelle puiser pour de nouveaux raisonnements. Une démonstration peut réutiliser un résultat déjà établi dans la bibliothèque, avec les définitions et les hypothèses qui l’accompagnent. L’intérêt du projet tient à cette possibilité de réemploi, au-delà du nombre de lignes produites. Une preuve correcte peut traduire le mauvais énoncé

Le fonctionnement de Lean diffère de celui d’un chatbot qui propose une explication mathématique. Son noyau vérifie qu’une preuve respecte les règles logiques et établit l’énoncé écrit dans le langage formel. La documentation de Lean sur la validation des preuves distingue explicitement cette validité du sens que l’on voulait donner au théorème.

Si une traduction ajoute une hypothèse absente du texte original, la preuve obtenue peut être correcte tout en établissant un résultat plus restreint. De même, une définition mal choisie peut déplacer le sens du problème. Le contrôle automatique ne dispense donc pas d’examiner les énoncés et les objets mathématiques utilisés.

C’est la fonction de la séparation entre StacksCore et StacksFrontier. Selon les responsables, le premier ensemble a été relu par des humains, comparé au Stacks Project et retravaillé selon les conventions de Mathlib. Le second contient les formalisations produites par les agents, dont la relecture humaine reste à effectuer. Le fichier de description du projet présente l’état de la revue comme autoévalué.

Les auteurs déclarent aussi ne pas utiliser de preuve laissée en attente avec la commande « sorry », ni d’axiomes supplémentaires aux fondements standards retenus. Ces engagements décrivent les conditions du contrôle annoncé. Ils ne constituent pas, à eux seuls, une revue indépendante de la correspondance avec l’ensemble du texte source. Une couverture annoncée dont le périmètre est précisé

La formule de lancement évoque la formalisation de l’intégralité du Stacks Project. Les documents du dépôt apportent des précisions : le README revendique la couverture des éléments ayant un contenu formalisable, tout en laissant des exemples, exercices et remarques comme tâches aux contributeurs. Le fichier descriptif indique une version précise du texte source, les chapitres 1 à 109 et l’exclusion des exercices ainsi que des chapitres obsolètes.

Ces indications délimitent la revendication de couverture. Le volume de code ne mesure ni la proportion déjà relue par des humains ni la qualité de chaque traduction. Le dépôt compte, selon ses responsables, environ 63 000 modules ; sa compilation complète demande du temps et beaucoup de mémoire. Un service de cache des modules compilés est annoncé comme prévu.

Les contributions attendues portent autant sur la revue que sur les ajouts. Le guide de contribution demande de conserver la généralité de l’énoncé original et de signaler un problème plutôt que de l’affaiblir pour réussir la preuve. Le passage de StacksFrontier à StacksCore constitue l’un des travaux proposés à la communauté. Le projet original conserve ses propres règles

La bibliothèque Lean publiée par Axiom et l’ouvrage dont elle part sont deux projets distincts. Le premier est distribué sous licence Apache 2.0 ; le second relève de la GNU Free Documentation License. Les nouvelles contributions au dépôt de formalisation passent par ses mainteneurs, avec une proposition préalable pour les travaux de formalisation ou de revue.

Le contexte du projet original est différent. Dans son billet « No AI for now », daté du 21 octobre, Johan de Jong demandait de ne pas envoyer de commentaires ou de propositions de modification contenant du matériel rédigé par IA. Ce texte précède l’annonce d’Axiom : il ne peut pas être présenté comme une réaction à cette publication.

Le mathématicien indiquait vouloir continuer à mettre à jour et à corriger