La cohérence de New Foundations — une preuve mathématique ardue vérifiée avec Lean

 (leanprover-community.github.io)
1 points par GN⁺ 2024-04-24 | 1 commentaires | Partager sur WhatsApp
  • La partie difficile de la preuve de cohérence de la théorie des ensembles New Foundations, proposée par Quine en 1937, a été vérifiée avec Lean, et le théorème central est consigné dans ConNF/Model/Result.lean
  • L’approche consiste à exploiter le résultat selon lequel la cohérence de New Foundations et celle de Tangled Type Theory (TTT) sont équivalentes, puis à construire formellement un modèle de TTT dans Lean
  • La construction d’un modèle de TTT est rendue difficile par l’extensionalité, qui exige que les ensembles soient déterminés de manière unique par leurs éléments de types inférieurs
  • La construction du modèle utilise des types de base, des t-sets, des permutations admissibles, un support petit et une preferred extension ; pour contrôler la taille des types avec μ, le freedom of action theorem est nécessaire
  • Le noyau de Lean vérifie la preuve formalisée, mais ne garantit pas que les énoncés formels correspondent au sens anglais visé ; l’interprétation du résultat nécessite donc de vérifier la traduction

Vérification dans Lean de la cohérence de New Foundations

  • En 1937, Quine a proposé la théorie des ensembles New Foundations, et Randall Holmes affirme depuis 2010 disposer d’une preuve de sa cohérence
  • Ce projet se concentre sur la vérification, avec le prouveur interactif de théorèmes Lean, de la partie difficile de la preuve de Holmes, afin d’établir la cohérence de New Foundations
  • La preuve est terminée, et l’énoncé du théorème est consultable dans ConNF/Model/Result.lean
  • Des ressources associées sont également fournies

Exécuter le code en local

  • Pour une exécution locale, il suffit d’installer elan, de cloner le dépôt, puis d’exécuter la commande suivante à la racine du dépôt
lake exe cache get
  • Le code peut ensuite être exploré dans un éditeur comme Visual Studio Code, et compilé directement en ligne de commande avec lake build

Le lien entre New Foundations et TTT

  • New Foundations est réputée cohérente si et seulement si Tangled Type Theory (TTT) est cohérente
  • Le projet a construit formellement un modèle de TTT dans Lean, ce qui permet d’obtenir, comme conclusion sur papier, la cohérence de New Foundations, c’est-à-dire Con(NF)
  • Le travail s’appuie sur plusieurs documents de preuve de Holmes, mais de nombreux changements et ajouts ont été nécessaires pour l’adapter à la théorie des types de Lean

Bases de la vérification Lean et précautions d’interprétation

  • Le projet dépend de mathlib, la bibliothèque mathématique communautaire écrite en Lean
  • Grâce à mathlib, des résultats familiers sur les cardinaux ou les groupes peuvent être utilisés dans le projet sans devoir être redémontrés
  • Les définitions et théorèmes de mathlib et de ce projet sont vérifiés par le noyau de confiance de Lean
    • Le noyau de Lean vérifie par calcul que les preuves construites sont effectivement correctes
  • En revanche, Lean ne peut pas vérifier que les énoncés formels correspondent bien à leur équivalent anglais attendu
    • Lorsqu’on tire des conclusions à partir du code, il faut examiner attentivement la traduction entre les descriptions en anglais et les énoncés formels

Structure et difficultés de Tangled Type Theory

  • TTT est une théorie des ensembles à plusieurs sortes dotée de l’é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
  • Les conditions de formation des formules sont limitées par les types
    • x = y est bien formée lorsque x et y ont le même type
    • x ∈ y est bien formée lorsque le type de x est inférieur au type de y
  • La difficulté centrale vient de l’axiome d’extensionalité de TTT
    • Un ensemble de type α doit être déterminé de manière unique par les éléments de n’importe quel type β < α
    • Par exemple, si deux ensembles de type α sont différents, alors, pour tout β < α, ils doivent avoir des éléments de type β différents
  • Cette exigence rend la construction d’un modèle de TTT plus délicate que celle d’un simple modèle de théorie des ensembles

Principales étapes de la construction du modèle

  • Construction des types de base

    • On prend λ comme ordinal limite, κ > λ comme ordinal régulier, et μ > κ comme cardinal fortement limite dont la cofinalité est au moins κ
    • Un ensemble de taille inférieure à κ est appelé small
    • On construit d’abord le base type de niveau -1, un type auxiliaire situé sous tous les types du modèle
    • Les éléments de ce type sont appelés atoms, mais il ne s’agit pas d’atomes au sens de ZFU ou NFU
    • Il y a μ atoms, partitionnés en litters de taille κ

  • t-sets et permutations admissibles

    • À chaque niveau de type α, on construit la collection qui deviendra les éléments du modèle de TTT ; elle est appelée t-set
    • On construit simultanément un groupe de permutations agissant sur les t-sets, les allowable permutations
    • La relation d’appartenance est préservée sous l’action des allowable permutations
    • Chaque t-set est choisi de façon à posséder un support pour l’action des allowable permutations
    • Le support est un petit ensemble d’objets appelés addresses
    • Si une allowable permutation fixe tous les éléments du support, elle fixe aussi le t-set

  • Ajuster l’extensionalité avec la preferred extension

    • Chaque t-set de niveau α possède une preferred extension d’un certain type β < α
    • On peut reconstituer, à partir des éléments du t-set, l’extension qui est préférée, et les extensions des autres types inférieurs sont dérivées de cette β-extension
    • Cette structure sert à satisfaire l’axiome d’extensionalité de TTT

  • Contrôle de la taille des types

    • Chaque type α ne peut être construit qu’avec, entre autres, l’hypothèse que la taille de tout type β < α est exactement μ
    • Il est facile de prouver que la collection des t-sets de niveau α a une taille au moins égale à μ ; il faut donc montrer qu’elle en a au plus μ
    • Pour cela, on montre qu’il n’existe pas beaucoup de descriptions fondamentalement différentes des tangles sous l’action des allowable permutations
    • Cette étape nécessite le freedom of action theorem, un lemme technique qui permet de construire les allowable permutations
    • Le résultat principal de cette section se trouve dans ConNF.mk_tSet

  • Finalisation inductive et vérification des axiomes

    • Le processus ci-dessus est exécuté récursivement pour générer, à chaque niveau de type α, le type des tangles
    • C’est une étape simple en théorie des ensembles, mais, dans la théorie des types, elle demande beaucoup de travail, car plusieurs hypothèses d’induction nécessaires sont imbriquées les unes dans les autres
    • On vérifie ensuite que la construction est un modèle de TTT en contrôlant qu’elle satisfait l’axiomatisation finie de la théorie
    • Le projet utilise l’axiomatisation finie du schéma de compréhension NF due à Hailperin, convertie en une axiomatisation finie de TTT
    • Le fichier de résultats se trouve dans le fichier des résultats
    • Ce choix est arbitraire ; avec l’infrastructure déjà construite, d’autres axiomatisations finies pourraient aussi être prouvées facilement

À lire aussi

1 commentaires

 
GN⁺ 2024-04-24
Avis Hacker News

  • Je pense que le risque qu’une preuve en Lean soit incorrecte est très faible.
    Cela dit, indépendamment des bugs de Lean, il existe un risque bien connu aussi bien en vérification logicielle qu’en mathématiques : il faut lire précisément la conclusion pour vérifier que la proposition réellement nécessaire a bien été démontrée.
    J’ai lu attentivement la conclusion finale de Wilshaw, et j’estime qu’elle démontre bien ce qu’il fallait démontrer.

    • L’article dit quelque chose de similaire : toutes les définitions et tous les théorèmes de mathlib et de ce projet ont été vérifiés par le noyau de confiance de Lean, qui a validé computationnellement que la preuve que nous avons construite est effectivement correcte.
      Mais Lean ne peut pas vérifier que les énoncés des définitions et des théorèmes correspondent à leur formulation anglaise prévue ; il faut donc faire attention à la traduction depuis l’anglais lorsqu’on tire des conclusions du code de ce projet.

    • Le problème que j’évoque est lié aux inquiétudes concernant les bibliothèques : quand on utilise un concept défini, il faut être sûr que sa définition est correcte, c’est-à-dire que ce dont on a vraiment besoin a bien été démontré.
      La formalisation de Wilshaw utilise certes des bibliothèques, mais elle n’est pas vulnérable à cette objection. Ce qui a été prouvé, c’est qu’un certain concept défini satisfait un paquet précis de formules de logique du premier ordre, et s’il existe un prédicat satisfaisant ces formules, alors NF est cohérente.

    • Un autre risque est un bug de Lean lui-même. Ce n’est pas sans précédent dans les prouveurs de théorèmes 1.
      Il peut être difficile de tomber dessus par hasard, mais les grandes collaborations où des personnes quelconques remplissent des étapes, comme dans 3, prennent de plus en plus d’ampleur. On pourrait commencer à s’inquiéter d’un scénario où quelqu’un exploiterait un bug qu’il a découvert pour remplir une étape et saboter le résultat.

    • Du point de vue des fondements, il est aussi important que cette preuve soit une preuve d’équicohérence entre NF et le noyau de Lean. Le noyau de Lean lui-même est relu par des humains.
      Les prouveurs de théorèmes mécanisés préservent le niveau de correction qui leur est injecté par des humains ou par d’autres systèmes externes.

  • Si je ne me trompe pas, cela semble être le premier cas où un assistant de preuve clarifie le statut d’une preuve difficile restée ambiguë pendant des années.
    Il y a déjà eu des projets de vérification de preuves existantes où un logiciel non fiable prenait en charge une grosse partie calculatoire, comme le théorème des quatre couleurs dans Coq, mais il me semble que c’est la première fois que le statut épistémologique même du résultat était incertain dans la communauté mathématique au sens large.

  • Quelqu’un pourrait-il expliquer dans les grandes lignes ce qu’il y a de spécial ou de nouveau dans la formalisation de la théorie des ensembles « New Foundations » par rapport aux autres formalismes ?
    À défaut, un lien vers une explication lisible par un étudiant de licence en maths ou par un ingénieur m’irait aussi.

    • Je viens de modifier l’article Wikipédia, il devrait maintenant être un peu plus lisible : https://en.wikipedia.org/wiki/New_Foundations
      Le point central, selon moi, est l’existence d’un ensemble universel. Dans mon cas d’usage, les systèmes de types des langages de programmation, un tel ensemble universel est très utile.
      Les divers contournements des systèmes existants, comme les univers cumulatifs ou le type-in-type, ne sont pas satisfaisants. À la place, on peut simplement vérifier que les signatures de types sont stratifiées, puis oublier que les types ont des niveaux numériques.
    • Ce que je trouve vraiment élégant dans NF, c’est la manière dont elle ajuste l’axiome de sélection de sous-ensembles pour que « l’ensemble de tous les ensembles » ne provoque pas le paradoxe de Russell.
      En gros, elle exige que le prédicat utilisé pour choisir un sous-ensemble respecte un système de types très léger. « x n’est pas un élément de lui-même » n’est pas une question bien typée dans un système de types raisonnable et, en particulier, ne satisfait pas non plus l’exigence de « stratifiabilité » de NF ; on ne peut donc pas construire l’ensemble du paradoxe de Russell, c’est-à-dire l’ensemble de tous les ensembles qui ne se contiennent pas eux-mêmes.
    • Un des « bons » côtés de NF est qu’elle n’a que deux axiomes/schémas d’axiomes : 1) les ensembles qui ont les mêmes éléments sont égaux, 2) à toute propriété stratifiable arbitraire correspond l’ensemble de toutes les choses qui possèdent cette propriété.
      La définition de « stratifiable » n’est pas très compliquée non plus. À l’inverse, ZF a huit axiomes/schémas d’axiomes qui paraissent assez ad hoc.

  • Je me demandais quelle était la différence fondamentale entre Coq et Lean, et s’ils fonctionnaient sur le même type de logique, et je suis tombé sur cet article 1.
    Je n’ai presque rien compris à cette discussion et je n’utilise pas vraiment l’un ou l’autre. S’il y a des explications supplémentaires à donner à ce sujet, ou des comparaisons avec d’autres assistants de preuve, je serais intéressé.

    1 https://proofassistants.stackexchange.com/questions/153/what...

  • Les partisans de Lean me semblent employer des formulations un peu excessives. Lean n’est pas une méthode de preuve supérieure, comme on le suggère souvent, mais une manière alternative de prouver.
    Quand on essaie d’apprendre Lean, on comprend vite que c’est un langage de programmation et un système avec ses propres bugs, et qu’il dépend fortement de plusieurs piles de bibliothèques écrites par d’autres humains. Ces bibliothèques incorporent des choix, et peuvent aussi contenir des lacunes ou des bugs.
    C’est pourquoi je ne suis pas d’accord avec les formulations du type « Lean a dit que cette preuve était bonne ». Une formulation plus exacte et honnête serait, à mon avis, que des mathématiciens humains ont vérifié la preuve rédigée, puis qu’un humain l’a traduite en Lean, où elle a également été vérifiée. Dire que Lean fournit l’unique validation en or n’est pas forcément exact, ou du moins je n’ai pas vu d’explication allant dans ce sens. Le sous-titre, « Numérisation de la preuve de Randall Holmes », me semble être la formulation la plus juste.

    • À mon avis, dans un système fort comme Lean, une preuve vérifiée par machine est de loin supérieure à une preuve vérifiée uniquement par des humains. Les humains sont remarquables, mais ils s’ennuient et ratent des détails.
      Ce n’est pas seulement une affirmation théorique. Les gens ont lu les Éléments d’Euclide pendant plus de deux millénaires avant de remarquer des axiomes manquants. C’est le genre d’erreur fondamentale qu’un système de vérification de preuves mécanisé fonctionnant correctement aurait immédiatement fait apparaître.
      Il arrive aussi souvent que des preuves mathématiques publiées se révèlent fausses par la suite. À mesure que les mathématiques deviennent plus sophistiquées, il devient de plus en plus difficile pour les humains de vérifier correctement chaque étape. Les machines ne sont pas encore aussi bonnes que les humains pour produire des preuves, mais pour les vérifier, elles sont sans équivalent.
      Il existe aussi des systèmes qui « concurrencent » Lean, donc je ne dirais pas que Lean est « la seule vraie voie ». Par exemple, j’aime aussi Metamath. Cela dit, la « concurrence » entre ces systèmes mérite des guillemets. Chacun a ses avantages et ses inconvénients, et beaucoup de gens apprécient, utilisent ou contribuent à plusieurs systèmes. Tous peuvent vérifier des théorèmes avec un degré de rigueur irréaliste pour des humains.

    • Il peut y avoir des bugs, mais ce qu’il faut faire confiance, si je comprends bien, c’est uniquement au noyau.
      Si « plusieurs piles de bibliothèques écrites par d’autres humains » désigne mathlib, je ne pense pas que ce soit correct. Le code de mathlib est lui aussi compilé en code traité par le noyau.
      Le brouillon de l’article sur le site 0 renforce ce point : Lean est un gros projet, mais pour garantir qu’une preuve acceptée est correcte, il suffit de faire confiance au noyau. Même si une tactique produit un terme de preuve incorrect, le noyau a l’occasion de détecter l’erreur avant d’accepter la preuve.

    • La différence, avec Lean, c’est qu’il suffit de faire confiance au noyau. Le reste est construit par-dessus. Si le noyau est sain, tout le reste l’est aussi.
      C’est très différent d’un langage de programmation classique. Dans un langage classique, des bugs peuvent s’introduire à tout moment. C’est aussi très différent des mathématiques, où n’importe quel lemme auxiliaire peut contenir une erreur.

    • Ce qui est formidable avec les prouveurs de théorèmes, c’est que, à supposer que le noyau soit correct, une preuve erronée ne compile même pas.
      En matière de preuves, il n’y a pas de bugs qui n’apparaissent qu’à l’exécution comme dans les logiciels traditionnels. Il n’y a tout simplement pas d’exécution.
      On peut aussi utiliser Lean comme un langage de programmation « ordinaire », et dans ce cas il existe un risque de bugs à l’exécution, mais ce n’est pas ce dont il s’agit ici.

    • Vous comprenez mal les prouveurs de théorèmes. Ce n’est pas une histoire du type « toutes les abstractions fuient ». Il n’est pas nécessaire de faire confiance aux bibliothèques : il suffit de faire confiance au noyau.
      Faire confiance au noyau n’est pas trivial, mais c’est un grand saut par rapport aux preuves informelles. Dans une preuve informelle, on doit réellement faire confiance à la « bibliothèque », c’est-à-dire à la culture et aux connaissances des autres, parce qu’il n’existe pas de moyen pratique de tout faire redescendre jusqu’aux axiomes.

  • ZFC est mort, vive NF ?
    En tant que mathématicien amateur qui utilise surtout les ensembles comme langage commun pour expliquer d’autres choses, je ne sais pas très bien quelles implications cela a pour le champ plus large des mathématiques. Surtout si l’utilité de NF est comparable à celle de ZFC et de ses variantes existantes.
    S’attend-on à ce que NF devienne aussi populaire que ZFC dans la preuve mécanisée ? L’existence de l’ensemble universel me paraît plus intuitive, et au moins cette preuve ravive mon intérêt personnel pour la formalisation.

    • Du point de vue d’un amateur naïf, comme tout modèle de ZFC peut être étendu en un modèle de NF, ce résultat de cohérence relative semble rendre NF au moins aussi utile que ZFC.
      Mais NF ne deviendra probablement pas beaucoup plus utile, sauf dans l’un des cas suivants :

      1. On prouve que NF est contradictoire. Alors ZFC l’est aussi. Les étoiles du ciel nocturne commencent à s’éteindre une à une ;)

      2. On prouve que ZFC est contradictoire. Alors il reste encore une chance que NF soit cohérent. Il faudra croiser les doigts.

      Bien sûr, il est tout à fait possible que je passe à côté d’avantages plus pratiques de « qualité de vie » propres à NF, comme la possibilité de parler de classes propres, ou l’évitement du paradoxe de Russell grâce aux formules stratifiées.

    • Il n’y a aucune intention de promouvoir NF comme système de fondements indépendant. NF est un système assez particulier.
      Cela dit, si quelqu’un voulait le défendre, ce résultat de cohérence permet au moins de dire qu’on ne court pas un risque plus grand qu’en ZFC d’aboutir à une contradiction.

  • J’aime vraiment beaucoup ça.
    Je me demande si l’on ne finira pas par aboutir à des preuves collaboratives et à de la « correction de bugs », au point que les mathématiques deviennent un processus comparable au code sur GitHub.

  • J’aimerais avoir du temps libre pour suivre le projet mathlib. C’est vraiment génial.
    Y a-t-il un moyen d’y participer, même de façon très informelle ?

  • Je ne suis pas du domaine, mais n’y avait-il pas le théorème de Gödel selon lequel tout système suffisamment puissant ne peut pas démontrer sa propre cohérence ?

    • Vous pensez sans doute aux théorèmes d’incomplétude de Gödel : https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
      Cela dit, même si un système X ne peut pas prouver sa propre cohérence, un système Y plus puissant peut prouver la cohérence de X. Et un autre système encore plus puissant peut à son tour prouver la cohérence de Y. On obtient ainsi une chaîne où chaque système prouve la cohérence d’un système plus faible
      Cela ne prouve pas que le système soit absolument cohérent. Si Y est contradictoire, il peut prouver aussi bien que X est cohérent que le contraire. Cela reste tout de même utile. Après tout, l’une des raisons pour lesquelles nous utilisons Y est précisément que nous n’y connaissons pas de contradiction. Les systèmes formels peuvent souvent être contradictoires de manière subtile ; donc « cohérent sous l’hypothèse qu’un autre système est cohérent » est bien préférable à « aucune preuve de cohérence »
    • Ici, le système ne prouve pas sa propre cohérence. Sa cohérence est prouvée dans un autre système plus puissant
    • Ce qui est intéressant, c’est que même si un système puissant pouvait prouver sa propre cohérence, cela ne nous apprendrait rien à lui seul
      Un système contradictoire peut aussi prouver sa propre cohérence. Donc, même si un système possède une preuve interne de sa cohérence, on ne sait toujours pas s’il est réellement cohérent
    • On peut comprendre cette preuve comme disant : « si Lean 4 est cohérent, alors New Foundations l’est aussi ». Cela ne contredit pas les théorèmes d’incomplétude de Gödel
    • Le système dont il est question ici ne semble pas chercher à prouver ses propres hypothèses de base, mais plutôt à construire par-dessus un ensemble d’hypothèses existantes. Le théorème auquel vous pensez ne devrait donc pas s’appliquer

  • La discussion Reddit à laquelle participe l’une des personnes qui l’ont réalisée vaut aussi le détour 0

    https://old.reddit.com/r/math/comments/1ca6bj8/new_foundatio...