La cohérence de New Foundations – une démonstration mathématique ardue prouvée avec Lean

Here is a summary of the key points from the given article, organized using Markdown:

Preuve de cohérence de la théorie des ensembles New Foundations

• Randall Holmes affirme depuis 2010 avoir démontré la cohérence de la théorie des ensembles "New Foundations (NF)", proposée par Quine en 1937
• Ce dépôt prouve que NF est effectivement sans contradiction en vérifiant, à l’aide du démonstrateur de théorèmes interactif Lean, les parties difficiles de la preuve de Holmes
• La preuve est désormais terminée, et l’énoncé du théorème se trouve dans ConNF/Model/Result.lean

Objectif

• On sait que NF est cohérente si et seulement si Tangled Type Theory (TTT) est cohérente
• La cohérence de NF est prouvée en construisant formellement dans Lean un modèle de TTT
• Le travail s’appuie sur plusieurs versions de la preuve de Holmes, mais de nombreuses modifications et additions ont été nécessaires pour la rendre compatible avec la théorie des types de Lean
• Ce projet dépend de mathlib, la bibliothèque mathématique communautaire écrite pour Lean, ce qui permet d’utiliser directement des résultats familiers sur les cardinaux ou les groupes sans devoir les redémontrer
• Le noyau fiable de Lean a vérifié toutes les définitions et tous les théorèmes de mathlib ainsi que de ce projet, mais Lean ne peut pas vérifier si les descriptions des définitions et théorèmes correspondent bien aux explications anglaises voulues ; il faut donc être prudent dans l’interprétation du code du projet en langage naturel

Tangled Type Theory (TTT)

• TTT est une théorie des ensembles multisorte munie de la relation d’égalité = et de la relation d’appartenance ∈
• Les sortes sont indexées par un ordinal limite λ, et les éléments de λ sont appelés indices de type
• La formule x = y est bien formée lorsque x et y ont le même type, et la formule x ∈ y est bien formée lorsque x a un type arbitrairement inférieur à celui de y
• L’un des axiomes de TTT est une extensionalité selon laquelle un ensemble de type α est déterminé de façon unique par ses éléments de type β pour tout β < α
• Par exemple, si deux ensembles de type α sont distincts, alors pour tout β < α ils possèdent des éléments distincts de type β, ce qui rend difficile la construction d’un modèle de TTT

Stratégie

• La construction du modèle suit globalement la stratégie suivante :

  • Construction des types de base

    • On fixe λ comme ordinal limite, κ > λ comme ordinal régulier, et μ > κ comme cardinal fortement limite de cofinalité au moins κ
    • Les ensembles de taille inférieure à κ sont dits petits
    • Au niveau -1, on construit un type auxiliaire appelé type de base, situé en dessous de tous les types qui feront finalement partie du modèle
    • Les éléments de ce type sont appelés atomes (mais pas au sens de ZFU ou de NFU) ; il y a μ atomes, répartis en litters de taille κ

  • Construction de chaque type

    • À chaque niveau de type α, on produit une collection d’éléments du modèle visé de TTT, parfois appelés t-ensembles
    • On construit un groupe de permutations appelé permutations autorisées, qui agit sur les t-ensembles
    • La relation d’appartenance est préservée par l’action des permutations autorisées
    • Chaque t-ensemble est astreint à avoir un support pour l’action des permutations autorisées ; ce support est un petit ensemble d’objets appelé adresses, tel que dès qu’une permutation autorisée fixe tous les éléments du support, elle fixe aussi le t-ensemble
    • À chaque t-ensemble du niveau α, on associe une extension privilégiée de type β < α, à partir de laquelle on peut retrouver, pour les éléments du t-ensemble, quelle extension est privilégiée
    • Les extensions de ces t-ensembles dans d’autres sous-types peuvent être déduites de la β-extension, ce qui permet de satisfaire l’axiome d’extensionalité de TTT

  • Contrôle de la taille de chaque type

    • Chaque type α ne peut être construit qu’en supposant, entre autres hypothèses, que tous les types β < α ont exactement pour cardinalité μ
    • Il est facile de montrer qu’au niveau α, la collection des t-ensembles a une cardinalité d’au moins μ ; il faut donc montrer que cet ensemble a au plus μ éléments
    • On y parvient en montrant qu’il n’existe pas tant de descriptions fondamentalement différentes de l’enchevêtrement sous l’action des permutations autorisées
    • Cela nécessite le théorème de liberté de l’action, un lemme technique permettant de construire des permutations autorisées
    • Le principal résultat de cette section se trouve ici

  • Clôture de l’induction

    • En exécutant récursivement le processus ci-dessus, on peut générer des types enchevêtrés à tous les niveaux de type α
    • C’est une étape facile en théorie des ensembles, mais qui demande beaucoup de travail en théorie des types à cause de l’interdépendance des diverses hypothèses d’induction nécessaires
    • On vérifie ensuite que notre construction produit bien un modèle de TTT satisfaisant une axiomatisation finie de la théorie
    • Nous avons choisi de convertir l’axiomatisation finie de Hailperin du schéma de compréhension de NF en une axiomatisation finie de TTT, présentée dans le fichier de résultats
    • Ce choix reste toutefois arbitraire, et l’infrastructure déjà en place permettrait de démontrer facilement d’autres axiomatisations finies

L’avis de GN⁺

• Cette preuve est très significative, car elle démontre formellement la cohérence de la théorie des ensembles NF, qui n’était jusqu’à présent connue qu’à un niveau très abstrait. C’est important non seulement pour les mathématiques pures, mais aussi comme illustration de progrès concrets dans les assistants de preuve et la démonstration automatique de théorèmes
• Le travail de formalisation avec Lean garantit la précision et l’exhaustivité de la preuve, mais il peut aussi être difficile à comprendre pour les mathématiciens, car il est rédigé dans un langage qui leur est peu familier. Un effort parallèle pour expliquer clairement les idées centrales de la preuve en langage naturel serait souhaitable
• Les explications intuitives du contexte théorique restent également limitées : pourquoi l’étrange axiome d’extensionalité de TTT est nécessaire, quelle est sa relation avec d’autres théories des ensembles, etc. En complément de la preuve formelle, une discussion du contexte philosophique et historique aiderait à mieux comprendre la théorie NF
• D’autres pistes de recherche paraissent aussi intéressantes, par exemple la relation entre le modèle construit et les modèles standard de la théorie des ensembles ZFC, ou encore la manière dont la cohérence de NF se relie à celle d’autres systèmes axiomatiques
• Un tel exemple de formalisation dans Lean d’une preuve aussi complexe pourrait servir de référence pour l’automatisation des preuves dans d’autres domaines des mathématiques. Si un travail similaire était tenté sur d’autres théorèmes dont la démonstration est encore mal connue, l’impact sur la communauté mathématique pourrait être considérable

[GN⁺]

Commentaires Hacker News

• Le risque qu’une preuve utilisant Lean soit erronée est très faible. Cependant, indépendamment des bugs de Lean, il faut lire attentivement la conclusion et vérifier qu’elle correspond bien à ce qui a réellement été démontré, un problème bien connu en vérification logicielle et en mathématiques.
• Ce cas semble être le premier où un assistant de preuve a été utilisé pour trancher l’état d’une preuve difficile. Il y avait déjà eu auparavant des projets vérifiant des preuves existantes comportant de gros éléments de calcul traités par des logiciels non fiables, mais ici il s’agirait du premier cas où le statut épistémologique du résultat était incertain dans la communauté mathématique.
• Des interrogations sont soulevées sur les différences fondamentales entre Coq et Lean, et sur le fait de savoir s’ils fonctionnent dans le même type de logique. La discussion associée mentionne des éléments difficiles à comprendre.
• Les partisans de Lean ont tendance à trop insister sur l’idée que Lean constituerait une meilleure méthode de preuve. Lean n’est qu’une méthode de preuve alternative ; en tant que langage de programmation et système, il a ses propres bugs et dépend fortement de diverses piles de bibliothèques écrites par d’autres.
• Il serait plus exact et plus honnête de dire non pas que Lean a affirmé qu’une preuve était bonne, mais que la preuve rédigée a été vérifiée par des mathématiciens humains, puis transposée dans Lean où elle a également été vérifiée. Présenter Lean comme fournissant une validation unique et quasi absolue n’est pas exact, ou du moins personne n’a vu de présentation le disant ainsi.
• Une demande est faite pour une explication générale de ce qui rend la formalisation de la théorie des ensembles "New Foundations" spéciale ou nouvelle par rapport à d’autres formalisations, dans un format accessible à un étudiant de licence en mathématiques ou à un professionnel de l’ingénierie.
• Certains se demandent si cette approche mènera finalement à des preuves collaboratives et à des "corrections de bugs", transformant les mathématiques en un processus similaire au code sur GitHub.
• Selon le théorème de Gödel, tout système suffisamment puissant ne peut pas démontrer sa propre cohérence ; une question est posée à ce sujet.
• Certains aimeraient continuer à suivre le projet mathlib mais manquent de temps. Ils se demandent s’il existe un moyen d’y participer de façon très passive.