vltanh/formalize-math-paper

Formalisation d'un article de mathématiques en Lean 4

Vous fournissez un projet Lean, accompagné de documents, dans lequel :

• chaque résultat que l'article prouve est prouvé par l'argument propre à l'article. Une preuve ne s'écarte de celle de l'article que lorsque c'est nécessaire, et chaque écart est signalé (Règles, « Preuves fidèles ») ;
• chaque résultat que l'article cite dans ses preuves est également prouvé : dans Mathlib, dans une autre bibliothèque publique, ou dans External/. Un résultat cité peut nécessiter des mathématiques qu'aucune bibliothèque Lean ne possède encore et que le projet ne peut raisonnablement construire. Un tel résultat devient une hypothèse nommée de toute énoncé qui l'utilise, et la formalisation indique alors clairement qu'elle est conditionnelle ;
• les énoncés disent ce que l'article dit, et tout écart est documenté ;
• lake build réussit sans sorry (sauf dans les énoncés de Challenge.lean, par conception), sans admit et sans axiome de projet. Chaque déclaration de la bibliothèque ne dépend que de propext, Classical.choice et Quot.sound ;
• REPORT.md audite l'article par rapport à la formalisation. Il se termine par ce qui vient ensuite : comment le sujet a évolué depuis l'article, comment ses résultats pourraient être étendus, généralisés ou renforcés, et comment ses preuves pourraient être simplifiées. README.md résume la formalisation, et CREDITS.md explique comment elle a été réalisée : la procédure, les agents et modèles, ainsi que le temps et l'effort (le journal d'exécution) ;
• un fichier privé NEXT.md, jamais publié sauf demande de l'utilisateur, répond à la question de savoir quel article l'utilisateur pourrait écrire ensuite après celui-ci : quelques candidats qui feraient chacun un article à part entière, explorés en profondeur (l'obstacle, les tentatives, les preuves, ce qui est déjà prouvé), et non une liste d'extensions incrémentales ;
• le projet est empaqueté pour Palomar et, avec l'autorisation de l'utilisateur, publié et passé par la pré-vérification de Palomar.

Le travail comporte deux étapes. Dans l'étape 1, formalisez tout ce que l'article lui-même prouve. Les résultats qu'il tire de la littérature peuvent être des axiomes temporaires. Dans l'étape 2, supprimez ces axiomes : prouvez-les, ou transformez ceux qui sont hors de portée en hypothèses énoncées. La configuration vient avant les deux étapes, et la vérification, le nettoyage, l'audit et l'empaquetage viennent après.

Principes

Ceux-ci expliquent les règles ci-dessous. Utilisez-les lorsqu'aucune règle ne couvre une situation.

• L'article est la source de vérité pour les énoncés et les arguments ; Lean juge de la correction. Un énoncé qui diffère de celui de l'article est une formalisation erronée, aussi propre que soit sa preuve. De même pour une preuve qui atteint l'énoncé de l'article par un autre argument : la formalisation vérifie les preuves de l'article, pas seulement ses affirmations. Examinez les énoncés par rapport à la source TeX avant quiconque ne les prouve. Comparez les preuves avec celles de l'article une fois qu'elles sont écrites. Ne modifiez jamais ni l'un ni l'autre en silence.
• Une formalisation que personne n'a compilée est un brouillon. Le Lean écrit de mémoire et jamais compilé contient souvent des noms de lemmes devinés, des signatures erronées et des lemmes auxiliaires faux. Compilez chaque fois qu'une chaîne d'outils Lean est disponible. Si ce n'est pas le cas, ou si l'utilisateur interdit la compilation, dites clairement que le résultat n'est pas vérifié.
• « Standard », « évident », « par symétrie », « routinier » nécessitent encore des preuves. Mathlib peut contenir le fait ; sinon, prouvez-le. Seul ce que l'article lui-même tire d'une autre source peut devenir un axiome.
• Externe indique d'où vient un résultat, pas qu'il est fiable. Un résultat cité vit dans External/ en raison de sa source. Il est prouvé comme tout le reste.
• Une hypothèse est une hypothèse, quelle que soit sa forme. Un résultat cité qui n'est pas prouvé est supposé, qu'il soit écrit comme un axiome, une hypothèse ou un champ d'une structure. Les axiomes ne sont pas autorisés. Les hypothèses sont autorisées lorsqu'un lecteur de l'énoncé peut voir chacune d'elles, sous le nom du résultat qu'elle suppose. Une structure qui mélange des données avec des théorèmes supposés cache ce dont dépend un résultat. De même pour un paramètre dont le type ressemble à une donnée mais contient un théorème.
• Les données viennent avec leur propriété définissante. Lorsqu'un énoncé prend un objet de l'article comme paramètre au lieu de le construire, il doit aussi exiger la propriété qui définit cet objet. Sinon, le théorème porte sur tout objet qui satisfait les autres hypothèses, ce qui est un énoncé différent.
• Les choix de représentation nécessitent des ponts. Les objets de Lean peuvent différer de ceux de l'article : des indices à partir de 0 au lieu de 1, des listes au lieu de familles indexées, une structure Mathlib regroupée au lieu d'un objet informel, un modèle concret au lieu d'une description « à isomorphisme près ». Lorsque c'est le cas, prouvez un lemme qui relie les deux, et documentez le choix. Ne supposez jamais que deux représentations sont équivalentes.
• Les constantes et les intervalles font partie des mathématiques. Les puissances, facteurs, parties entières inférieures et supérieures, inégalités strictes versus larges, les extrémités des intervalles et la soustraction tronquée sur ℕ décident si un énoncé est vrai.
• Rapportez honnêtement. Si une étape a été sautée, une preuve échoue, un énoncé a dû changer, ou une preuve a dû s'écarter de celle de l'article, dites-le et donnez la raison. L'audit n'est utile que s'il peut être fiable.
• Un trou dans une preuve n'est pas un énoncé faux. Lorsque la preuve de l'article utilise un fait que ses hypothèses ne donnent pas, l'énoncé peut encore être vrai. Cherchez un argument correct avant de conclure quoi que ce soit sur l'énoncé.
• Mesurez le travail. Les lecteurs et les registres demandent comment une formalisation a été réalisée. La réponse est peu coûteuse à enregistrer au fur et à mesure, et difficile à reconstruire après coup.

Règles

• N'affaiblissez ni ne modifiez jamais l'énoncé d'un résultat de l'article pour faire fonctionner une preuve. Si l'énoncé de l'article est faux, arrêtez le travail sur celui-ci et informez-en immédiatement l'utilisateur, avec le contre-exemple. D'autres travaux peuvent continuer entre-temps. Si l'utilisateur est d'accord, formalisez la version correcte la plus proche et enregistrez-la comme une erreur dans le rapport. Les erreurs typographiques évidentes sont la seule exception (ci-dessous).

• N'ajoutez jamais une hypothèse à un résultat de l'article parce que sa preuve semble en avoir besoin. En ajouter une affaiblit le résultat. N'en ajoutez une que lorsque l'énoncé lui-même a un contre-exemple, pas parce qu'une étape de la preuve échoue, puis suivez la règle précédente. Sinon, prouvez l'énoncé tel qu'imprimé, par un argument corrigé, et enregistrez le trou dans la preuve comme un élément-E. Si vous ne trouvez ni preuve ni contre-exemple, dites à l'utilisateur ce qui manque. Ils décident s'il faut continuer à travailler ou formaliser un énoncé plus faible, documenté comme une déviation.

• Preuves fidèles. Prouvez chaque résultat par la preuve de l'article : les mêmes affirmations intermédiaires, les mêmes constructions et scissions de cas, et les mêmes résultats antérieurs là où l'article les cite. Les résultats que la preuve de l'article cite forment sa route. La preuve formelle doit avoir la même route, et la vérification de la route (Phase 6) le confirme. Seuls les mécanismes peuvent différer : les tactiques, le lemme Mathlib qui ferme une étape routinière, l'ordre des étapes indépendantes, et les lemmes auxiliaires qui encapsulent une étape de l'article. Si Mathlib parvient à prouver un résultat numéroté, prouvez-le quand même par l'argument de l'article, à moins que l'article lui-même ne le traite comme connu (il le cite, ou le qualifie de standard).

• Ne vous écartez de la preuve de l'article que lorsque vous le devez, c'est-à-dire pour l'une de ces raisons et aucune autre :

  1. l'argument de l'article est erroné à cette étape, ou présente un trou à cet endroit, et ne peut pas être réparé selon ses propres lignes (l'étape est aussi un élément-E) ;
  2. l'étape nécessite des mathématiques que Lean ne possède pas et que le projet ne peut raisonnablement construire (comme pour les résultats cités hors de portée, ci-dessous), et un autre argument les évite ;
  3. l'étape n'a pas de sens dans une représentation que la formalisation doit utiliser (Principes), donc une traduction fidèle de celle-ci est un argument différent.

  Une preuve plus courte, plus élégante, plus générale ou plus automatique n'est pas une raison. Pas plus qu'une preuve plus facile à formaliser ou plus rapide à construire. Un argument plus simple que vous trouvez mérite néanmoins d'être conservé : enregistrez-le, avec une esquisse, pour la section « Et ensuite » du rapport (Phase 8), et prouvez le résultat par l'argument de l'article. Écartez-vous aussi peu que la raison l'exige : réparez l'étape, pas la preuve. Si un écart devait remplacer l'argument entier d'un résultat numéroté, pas seulement une étape, proposez-le d'abord à l'utilisateur, avec la raison. D'autres travaux continuent entre-temps.

• Signalez toujours chaque écart. Pour chacun, enregistrez ce que l'article fait, ce que la formalisation fait à la place, et quelle raison impose le changement. Enregistrez-le dans la docstring de la déclaration (« Écart par rapport à l'article : … »), dans le tableau des écarts du rapport, dans formalization.yaml (fidelity.divergences), dans tout texte compagnon, dans le fichier de différences enregistrées de la vérification de route lorsque la route change, et dans le prochain rapport d'état. Un écart manquant dans l'un de ces éléments est un défaut : trouvez-le et corrigez-le comme vous le feriez pour un énoncé modifié en silence.

• Résultats cités hors de portée. Un résultat cité peut nécessiter des mathématiques qu'aucune bibliothèque Lean ne possède. Si construire ces mathématiques dans le projet est un effort modéré, construisez-les. Sinon, le défaut est une formalisation conditionnelle : le résultat devient une hypothèse nommée de tout énoncé dont la preuve l'utilise. Appliquez le défaut sans demander, et signalez-le dans le prochain rapport d'état. Ne demandez à l'utilisateur que lorsque la construction des mathématiques manquantes serait un effort important mais réalisable : c'est à eux de décider s'il faut consacrer cet effort. Entre-temps, continuez les autres travaux sous le défaut. S'ils choisissent de le construire, planifiez le travail en couches. Chaque couche remplace certaines hypothèses par des constructions et des preuves à partir de plus basiques, et se termine dans un état qui peut être publié. Ces hypothèses sont les seules qui peuvent être ajoutées à un résultat de l'article sans contre-exemple. Ne présentez jamais une formalisation conditionnelle comme complète : son README, formalization.yaml et son rapport indiquent qu'elle est conditionnelle et listent ce qu'elle suppose.

• Coquilles dans les énoncés. Si un énoncé n'est faux qu'en raison d'une coquille évidente (un mauvais indice, un nom échangé, un - 1 manquant), et qu'une seule lecture peut être souhaitée, formalisez cette lecture immédiatement, dans la bibliothèque et dans le Challenge. Listez chaque correction dans le rapport et dans le prochain rapport d'état à l'utilisateur. Lorsque plus d'une correction est possible, traitez l'énoncé comme faux.

• Un lemme auxiliaire faux (que vous ou un brouillon avez introduit) nécessite un contre-exemple concret, vérifié dans Lean (decide, norm_num ou #eval) lorsque c'est possible. Ajoutez ensuite l'hypothèse minimale, mettez à jour ses appelants, et enregistrez le changement dans le message de commit.

• À la fin, il n'y a pas de sorry (en dehors de Challenge.lean), admit, axiome, native_decide ou implemented_by. native_decide ajoute un axiome, que Comparator rejette.

• Ne devinez jamais un nom ou une signature de Mathlib. Fouillez les sources épinglées dans .lake/packages/mathlib, ou utilisez #check, exact? et Loogle. Mathlib renomme et déprécie souvent les déclarations, et les avertissements de dépréciation nomment le remplacement.

• Si vous ne pouvez pas compiler (pas de chaîne d'outils, ou l'utilisateur l'interdit), écrivez le Lean sans le compiler. Vérifiez chaque nom, signature et chemin d'importation par rapport aux sources Mathlib épinglées, conservez l'ordre des énoncés d'abord, et étiquetez chaque résultat comme non vérifié. Quiconque compile le projet plus tard commence à la Phase 3.

• Exécutez un seul lake build à la fois par espace de travail. Les builds qui s'exécutent en même temps suppriment les fichiers .olean les uns des autres, et un éditeur ouvert sur le projet exécute ses propres builds lake setup-file. Si vous voyez « objet fichier … n'existe pas », réessayez plutôt que de modifier autour.

• Demandez avant toute action que d'autres peuvent voir : pousser, créer un dépôt, modifier la visibilité d'un dépôt, ouvrir ou fermer des demandes de tirage, supprimer des branches, exécuter la pré-vérification de Palomar, soumettre à Palomar, enregistrer. L'autorisation pour l'une de ces actions n'est pas une autorisation pour les autres.

• Les auteurs sont des personnes. Créditez les systèmes d'IA dans le README, dans CREDITS.md et dans la section automation de formalization.yaml, jamais en tant qu'auteurs ou mainteneurs.

• Tenez un journal d'exécution dès le début (voir « Journal d'exécution » ci-dessous). Rapportez-le dans CREDITS.md, dans formalization.yaml et dans les rapports d'état.

Flux de travail

Phase	Objectif	Fait quand
0. Configurer	enregistrer la tâche, poser les questions ouvertes	configuration enregistrée
1. Inventorier	connaître l'article : ses résultats, définitions, constantes, citations et d'où leurs preuves peuvent venir, fautes de frappe suspectées	liste de contrôle de travail complète
2. Projet	un projet Lean sur une version de Mathlib, avec le système de modules, organisé par section de l'article	lake build s'exécute
3. Énoncés	chaque définition et résultat numéroté énoncé, avec des preuves sorry ; le Challenge	les énoncés sont élaborés et passent une revue indépendante par rapport à l'article ; base de référence validée
4. Étape 1	prouver tout ce que l'article prouve, par les preuves de l'article	seuls les résultats cités subsistent, comme axiomes dans External/ ; chaque écart signalé
5. Étape 2	prouver les résultats cités	zéro axiome ; chaque résultat encore supposé est une hypothèse nommée
6. Vérifier	audit des axiomes, table des dépendances, vérification de la route, Solution et Comparator	scripts/Audit.lean et la vérification de route passent ; preuves comparées à celles de l'article ; Comparator accepte
7. Nettoyer	aucun avertissement, aucune hypothèse inutilisée, aucun nom trompeur, routes inchangées	la build ne montre que les sorry du Challenge ; la vérification de route passe toujours
8. Auditer	REPORT.md, README.md, CREDITS.md ; le NEXT.md privé	chaque résultat vérifié par rapport à la source TeX ; chaque candidat de suivi vérifié pour la nouveauté et par rapport à la barre
9. Empaqueter	CI, fichiers et vérifications Palomar ; publication et pré-vérification, avec permission	les vérifications locales de Palomar passent ; après publication, la pré-vérification rapporte status: pass

Validez à chaque jalon, avec un message qui dit ce qui a changé et pourquoi.

Phase 0 : Configurer

Enregistrez ceci. Ne demandez à l'utilisateur que ce que vous ne pouvez pas déterminer vous-même :

paper:            arXiv id et version (ou DOI) ; source TeX si disponible ; versions ultérieures

…

[truncé pour la traduction]