À la croisée des fondements des mathématiques, de l’informatique et de la topologie

Théorie homotopique des types

Hors-piste 7 décembre 2013  - Ecrit par  Antoine Chambert-Loir Voir les commentaires (13)

Toute l’année dernière, une cinquantaine de mathématiciens et informaticiens s’est réunie à l’Institute for Advanced Study de Princeton autour de Steve Awodey, Thierry Coquand et Vladimir Voevodsky pour réfléchir aux Fondations univalentes des mathématiques. Ce qui en est issu est peut-être bien une nouvelle révolution, à la croisée de l’informatique, de la théorie de l’homotopie et des fondements des mathématiques.

Une aventure d’un nouveau genre

Quitte à prendre le risque d’une généralisation forc(en)ée, les mathématiciens sont souvent des êtres solitaires qui, du fond de leur bureau, écrivent seuls des textes d’ampleur variable (10 à 100 pages, mais rarement plus). Et lorsqu’ils sont plus nombreux, c’est le plus souvent dans une espèce de solitude à quelques-uns : parfois chacun des auteurs écrit indépendamment une partie, parfois l’écriture est réellement à quatre mains. L’article est alors soumis au comité de rédaction d’une revue, ou, quand il est trop gros, d’une collection de monographies. Une fois la publication décidée, l’éditeur de la collection assure la fabrication et la diffusion de l’ouvrage en échange des droits de reproduction (et, parfois, de modestes droits d’auteur). Ensuite, si d’autres mathématiciens veulent étudier ce travail, il leur faut acheter (ou faire acheter par leur bibliothèque) la revue ou l’ouvrage auprès de l’éditeur.

En juin dernier, débarquait sur la planète maths un omni (objet mathématique non identifié) : 600 pages écrites de façon collective en 6 mois par 40 scientifiques de tous âges, originaires de toute la planète, sur un sujet de recherche essentiellement neuf !

Concrètement, tous ces auteurs ont passé un ou deux semestres de l’année universitaire 2012/2013 à l’Institute for Advanced Study de Princeton pour participer au programme spécial que cet institut organisait, programme au titre ésotérique de « univalent foundations of mathematics ». Reclus dans cette espèce de phalanstère, ils ont discuté, réfléchi, exposé leurs progrès sur le sujet qui les réunissait tous ; jusque-là, rien que d’assez normal en apparence.

Si ce n’est que ce sujet de recherches était essentiellement neuf, on y reviendra plus bas.

Et que ces mathématiciens ont saisi cette occasion pour nous livrer un gros et fascinant livre qui synthétise leurs progrès. Mais la méthode de travail était radicalement différente de celle que j’ai évoquéee plus haut. En effet, et c’est peut-être la première fois qu’un ouvrage scientifique les utilise de façon si massive, ils se sont appuyés sur les nouvelles technologies collaboratives d’usage courant en logiciel libre, telles qu’un site web, un blog, ou le logiciel de contrôle de versions distribué git. En clair, l’écriture du livre se faisait entièrement de façon électronique, les fichiers étaient partagés, le logiciel git se chargeant de vérifier les inévitables conflits, lorsque deux collègues veulent en même temps modifier le même passage. Même si un joli film d’animation montre qui, quand, comment chacun est intervenu sur les divers chapitres qui constituent l’ouvrage, et si certains contributeurs sont un peu mis en avant dans la présentation du livre, ce livre n’a pas vraiment d’auteur identifié.

En outre, ce livre est accessible librement via Internet (http://homotopytypetheory.org/) ; si on en souhaite une copie, le livre est imprimé à la demande via le site d’impression Lulu qui le produit pour une somme assez modeste (une vingtaine d’euros la version cartonnée). Enfin, le livre est publié sous une licence Creative Commons, qui permet à chacun d’en faire ce qu’il veut (ou presque), y compris de le modifier ou le revendre.

Mais les ouvrages collectifs ne datent pas d’hier. Les ouvrages de N. Bourbaki sont peut-être les plus fameux, mais on peut aussi citer celui de D. P. Parent, les deux volumes publiés par A. L. Besse, et, encore plus récemment les travaux de Pytheas Fogg, Benedictus Margaux ou Henri-Paul de St Gervais. De même, l’accès libre à la littérature scientifique constitue de nos jours un maillon extrêmement important de la diffusion de la science : les articles de recherche sont déposés sur des bases de données comme arXiv ou haL ; les articles plus anciens sont parfois numérisés par les éditeurs ou les pouvoirs publics et offerts au public, sur l’une des plates-formes telles que EuDML, Numdam, Gallica) ou le centre de numérisation de Göttingen.

Ainsi, même si ces éléments matériels suffisent peut-être à faire de ce programme une petite révolution du fonctionnement de la science, l’essentiel est bien ailleurs.
Venons-en donc au fond.

De quoi s’agit-il ? D’informatique. De mathématiques. De théorie de l’homotopie. De fondements. De vérifications de preuves. Tout ça résumé en un vocable un peu effrayant de « théorie homotopique des types ».

J’en ai lu trop peu (encore) pour résumer tout ce travail ; j’espère même ne pas faire de contresens. Mais même en n’ayant lu que le début de ce livre, je ressens avec certitude et enthousiasme qu’un nouvel et merveilleux univers mathématique est en train de naître. Alors les lignes qui suivent, qui ne manqueront pas d’être classées hors-piste par les éditeurs d’Images des maths, ont pour seul but de vous donner envie de vous ruer sur les sites indiqués plus haut et de commencer à lire ce livre par vous-mêmes.

Je reviendrai d’abord sur la théorie des ensembles et essaierai d’expliquer pourquoi, bien qu’elle soit au cœur des mathématiques quotidiennes, on ne peut pas trop la prendre au sérieux en tant qu’outil de formalisation des mathématiques.

La notion de catégorie permettra ensuite de discuter des ambiguïtés prévalentes en mathématiques, permettant une transition avec une évocation (d’apparence algébrique) de la théorie de l’homotopie supérieure.

J’expliquerai ensuite comment la théorie homotopique des types unifie ces idées
et conclurai avec l’aspect constructif de toute cette histoire, les vérifications de preuves assistées par ordinateur.

Théorie des ensembles

Depuis un peu plus de 100 ans, la vie mathématique est organisée autour des ensembles. C’est une théorie efficace, relativement concise, puisqu’il y a essentiellement un seul symbole (celui d’appartenance) en sus des symboles logiques — sans chercher à être minimal, disons les signes ∧ (et), ∨ (ou), ⇒ (implication), ⇔ (équivalence), = (égalité) — et peu d’axiomes (assez subtils).

Cependant, la théorie des ensembles a de nombreux défauts. Le premier est qu’elle suscite des questions ridicules et sans grand intérêt. Prenons l’exemple des entiers naturels et des entiers relatifs.

Les fondations des mathématiques sont une espèce de jeu de Lego où l’on démarre avec des briques d’apparence assez banale et où l’on chercherait à reproduire un modèle de l’univers. On agence ces briques pour « construire » (je mets des guillemets, mais les mathématiciens l’utilisent au sens propre) les objets mathématiques courants.
Il y a ainsi un moment où l’on dispose de l’ensemble $\mathbf N$ des entiers naturels, et où l’on doit construire celui, classiquement noté $\mathbf Z$, des entiers relatifs. Plusieurs constructions sont possibles. La plus simple consiste à dire qu’un entier relatif est un entier auquel on adjoint un signe ; dans cette version, $\mathbf Z$ est la réunion de l’ensemble $\mathbf N$ et d’une copie auxiliaire de l’ensemble $\mathbf N\setminus\{0\})$ qui représente les nombres strictement négatifs. Mais si l’on veut être précis (et à ce stade des fondations, il s’agit de l’être), il faut justifier pourquoi, alors qu’on dispose de l’ensemble $\mathbf N$, on peut trouver d’autres éléments « ailleurs », afin de former cette réunion disjointe. Une autre construction, un peu plus élégante, consiste à observer qu’un nombre relatif s’écrit soit $n-0$, soit $0-n$ ; on peut ainsi dire que $\mathbf Z$ est l’ensemble des couples $(m,n)$ de deux entiers naturels dont l’un des deux est nul ; mais la construction de l’addition est un peu alambiquée. La construction la plus élégante observe que l’on peut relâcher la condition que l’une des deux composantes du couple $(m,n)$ est nulle, le couple $(m,n)$ représentant toujours $m-n$, mais il faut alors introduire la relation (d’équivalence) selon laquelle $(m,n)$ est équivalent à $(m',n')$ si $m+n'=m'+n$ ; dans cette construction, un entier relatif est une classe d’équivalence de couples d’entiers, c’est-à-dire une partie de $\mathbf N\times\mathbf N$. Quoiqu’on enseigne en licence, a-t-on vraiment envie de penser au nombre $-3$ comme à l’ensemble $\{ (0,3); (1,4); (2,5);\dots\}$ ?

De même, dans chacune des trois constructions esquissées, l’ensemble $\mathbf Z$ qui est défini ne contient pas tout à fait les entiers naturels, mais seulement une copie conforme de ceux-ci. Des identifications sont nécessaires, identifications que les mathématiciens ignorent savamment, mais sur lesquelles il faudrait en théorie se pencher de temps en temps. « Cachez ce sein... » Cependant, les constructions sont rapidement de plus en plus compliquées et s’il convenait de garder trace de toutes ces identifications, personne ne le fait au-delà de deux-trois exercices d’entraînement.

La théorie des ensembles ne semble donc pas très compatible avec le courant de pensée constructiviste auquel l’avènement des ordinateurs et des systèmes de vérifications de preuve redonne une certaine actualité. Indépendamment de ces aspects informatiques, elle est aussi moins adaptée à l’étude de théories plus molles où des objets semblables (isomorphes) sont identifiables mais pas égaux ; en tout cas, où les identifications sont suffisamment nombreuses et riches pour ne pouvoir être ignorées.

J’ai en tête deux théories de ce genre : la théorie des catégories et la théorie de l’homotopie.

À ce point, le lecteur soupçonne probablement que le niveau mathématique va par moment décoller brutalement. C’est hélas le cas ; les exemples que je vais évoquer sont parfois enseignés au niveau master, donc peut-être ne vous diront-ils rien du tout. Mais, s’il vous plaît, n’arrêtez pas de lire ! Ou si vos yeux et votre cerveau le refusent, laissez vous aller et écoutez la musique qui s’en dégage...

Catégories

Si elle pose quelques problèmes de fondations au sein de la théorie des ensembles, la théorie des catégories est pour le moins un vocabulaire extrêmement efficace pour exprimer les relations entre divers types d’objets mathématiques, vocabulaire qui s’est imposé au cours de la seconde moitié du 20e siècle dans des domaines comme la théorie des représentations, la géométrie algébrique ou la topologie algébrique.

Les catégories contiennent des « objets », et les objets sont reliés par des « morphismes » qui se composent. Pensez aux groupes et aux morphismes de groupes, aux espaces topologiques et aux applications continues, aux espaces vectoriels sur un corps fixé (disons $\mathbf C$) et aux applications linéaires, etc. En outre, diverses catégories sont reliées par des « foncteurs » qui transforment à la fois objets et morphismes. On pourrait dire que les foncteurs sont des producteurs de reflets. Par exemple, la topologie algébrique associe à tout espace topologique ses groupes d’homologie, qui sont des groupes abéliens, les applications continues entre espaces topologiques étant transformées en morphismes de groupes. Et lorsqu’on démontre qu’un certain groupe d’homologie est nul, ou non nul, voire qu’on le calcule précisément, on observe un reflet de l’espace topologique qui nous intéresse, reflet qui est parfois la clé d’une propriété fondamentale.

Au sein d’une même catégorie, il est fréquent que les objets puissent être distincts mais « isomorphes ». De tels exemples arrivent déjà, et de façon fondamentale, dès les mathématiques de licence.

Les ensembles, par exemple. Il y a plein d’ensembles à un élément ; et pourtant, ils sont tous « pareils » : s’ils sont différents (l’ensemble $\{a\}$ est différent de l’ensemble $\{b\}$), leur point commun est de n’avoir qu’un seul élément. Mieux : entre deux ensembles à un élément, il y a exactement une bijection (tiens, voilà un autre ensemble à un élément...). Les choses sont plus amusantes avec les ensembles à deux éléments. Ils sont aussi essentiellement « pareils » puisqu’on peut trouver une bijection entre deux ensembles à deux éléments quelconques. La différence est qu’on peut trouver deux bijections : il y a deux bijections de l’ensemble $\{1,2\}$ sur l’ensemble $\{a,b\}$, celle qui applique $1$ sur $a$ et $2$ sur $b$, et celle qui applique $1$ sur $b$ et $2$ sur $a$. Il y a même deux bijections de l’ensemble $\{1,2\}$ dans lui-même. Quand le nombre d’éléments augmente, cela devient de plus en plus riche, et les bijections de l’ensemble $\{1,2,\dots,n\}$ à $n$ éléments sur lui-même constituent les $n!$ éléments du groupe symétrique $S_n$ « sur $n$ lettres ». De l’ambiguïté des identifications naît un morceau de la théorie des groupes...

De même, pensez aux espaces vectoriels, disons de dimension finie sur $\mathbf C$. C’est une catégorie très grosse car il y a énormément d’espaces vectoriels, même si l’on en restreint la dimension, et ce, pour la même raison qu’il y a énormément d’ensembles, même finis, même à un seul élément. Mais l’algèbre linéaire dit que la catégorie des espaces vectoriels n’est pas si compliquée que cela. D’abord, tout espace vectoriel est isomorphe à un espace de la forme $\mathbf C^n$ ; car tout espace vectoriel possède une base finie. Ensuite, l’entier $n$ est déterminé par l’espace, c’est sa dimension, car deux bases d’un même espace ont même cardinal. Bien sûr, il y a beaucoup d’isomorphismes : une fois qu’on en a choisi un, les autres diffèrent par composition avec un élément arbitraire du groupe $\mathrm{GL}_n(\mathbf C)$. Dit autrement, chaque fois que l’on effectue un changement de base, on ne change pas vraiment l’espace vectoriel, mais on le regarde vraiment différemment.

Aussi, et c’est peut-être pour cela que l’enseignement de licence peut garder quelque caractère concret, la catégorie des espaces vectoriels de dimension finie sur $\mathbf C$ est équivalente à une autre catégorie d’apparence bien plus simple : ses objets sont les entiers naturels $\{0,1,..\}$, et les morphismes d’un entier $n$ vers un entier $m$ sont les matrices $n\times m$ à coefficients dans $\mathbf C$.

Parfois, on veut construire une nouvelle catégorie à partir d’une ancienne (technique de localisation) en conservant les objets mais en modifiant les morphismes, typiquement en ajouter, en décrétant que certains sont des isomorphismes. La topologie algébrique, une des grandes branches de la géométrie, tente de classer les formes géométriques avec deux règles du jeu : d’une part, on ne tient pas compte de certaines déformations (les homotopies) et d’autre part, on essaie de réduire la complexité géométrique à des objets algébriques (les groupes d’homotopie), si ce n’est que le calcul de ces groupes d’homotopie, même pour des objets aussi simples que des sphères, s’avère un problème absolument intordable... Dans sa thèse, Jean-Pierre Serre avait fait faire un pas de géant au sujet en montrant comment raisonner sur ces groupes d’homotopie en décrétant qu’un morphisme de groupes abéliens était un isomorphisme dès que son noyau et son conoyau étaient finis. Par exemple, la multiplication par 2 de $\mathbf Z$ dans $\mathbf Z$ devient un isomorphisme. Une telle construction force à sortir de la théorie des ensembles, au sens où un morphisme entre deux groupes n’est plus (« est », au sens ontologique du terme) une application entre les deux groupes. Dans l’exemple précédent, le morphisme réputé être l’inverse de la multiplication par 2 de $\mathbf Z$ dans $\mathbf Z$ n’est en effet plus représentable par une application...

Homotopie

Utilisons cette transition pour passer à la théorie de l’homotopie.

Commençons par les lacets. Depuis Poincaré, on sait classifier les revêtements d’un espace topologique raisonnable à l’aide du groupe fondamental, dont les éléments sont les classes d’homotopie de lacets basés en un point (les homotopies fixant le point-base). Pour se débarrasser de l’hypothèse de connexité et des choix de points-base, il est commode d’introduire le groupoïde fondamental : c’est une catégorie dont les objets sont les points de l’espace topologique, un morphisme d’un point vers un autre étant une classe d’homotopie de chemins reliant le premier point au second (les homotopies préservant les extrémités), la composition des morphismes étant donnée par la juxtaposition des chemins.

Le groupe fondamental apparaît alors comme les morphismes du point-base vers lui-même, exactement comme $\mathrm{GL}_n(\mathbf C)$ était l’ensemble des isomorphismes de l’espace $\mathbf C^n$ vers lui-même.

Je n’ai décrit ici que le début de la construction. Par la définition même du groupoïde fondamental, les homotopies entre chemins sont elle-mêmes importantes, ce qui justifie de considérer, pour tout entier $n$, les applications du cube $[0,1]^n$ vers notre espace, et les homotopies entre ces applications qui sont des applications du cube $[0,1]^{n+1}$.

Cela donne lieu à une structure combinatoire à la fois très simple et très riche qu’on appelle un $\infty$-groupoïde. Très simple puisqu’il n’y est question que d’une suite d’ensembles reliés par des applications issues des inclusions des faces dans le cube. Très riche car cette structure contient tous les renseignements topologiques « mous » de l’espace dont on est partie.

Théorie homotopique des types

La théorie homotopique des types incorpore toutes ces idées. Tout d’abord, le concept de base n’est pas celui d’ensemble, mais celui de type, la relation d’appartenance ($x\in A$ pour dire que $x$ appartient à l’ensemble $A$) est remplacée par la variante $x:A$ qui dit que $x$ est un membre du type $A$. Un peu comme en théorie des ensembles, on construit un type pour les entiers, un type pour les booléens. Si $A$ et $B$ sont deux types, $A\times B$ est un type (qui représente la donnée d’un objet de type $A$ et d’un objet de type $B$) de même que $A+B$ (un objet de type $A$ OU un objet de type $B$) ou $A\to B$ (une application qui associe à un objet de type $A$ un objet de type $B$). Mais il y a des types d’un nouveau genre.

Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles pour décrire les fondements des mathématiques. Mais son utilisation donne alors une présentation assez différente. Tout d’abord, les théories mathématiques classiques ont deux étages : le premier est une machinerie générale de preuve, le second est l’axiomatisation de la théorie en question. Une des particularités de la théorie des types est de combiner objets et preuves. Les propositions, c’est-à-dire les assertions mathématiques, qu’elles soient vraies ou fausses, sont elles-mêmes des types ; un tel type est « vrai » s’il possède un membre. Ainsi, le type $p\to q$ représente la proposition que $p$ entraîne $q$, etc. De la sorte, la théorie des types est un socle formel possible pour le raisonnement mathématique en même temps qu’il en est un pour ses objets.

Le traitement de l’égalité entre deux objets manifeste une différence fondamentale entre théorie des types et théorie des ensembles. En théorie des types, la phrase mathématique qui énonce l’égalité entre l’objet $x$ et l’objet $y$ n’est bien formée qu’à la condition que $x$ et $y$ vivent dans un même type $A$. Par exemple, il n’est pas possible de former (sans même parler de démontrer bien sûr) la phrase « 3 = vrai » car 3 est un entier et vrai un booléen. Une présentation « typée » des objets mathématiques a en effet vocation à classifier ces objets, pour écarter d’emblée, syntaxiquement certaines phrases qui n’auraient pas de sens. En théorie des ensembles, l’énoncé « 3 = vrai » a un sens (et est faux, dès lors que les booléens sont codés comme les entiers 0 et 1) ; de même, il est (syntaxiquement) possible en théorie des ensembles de se poser des questions mathématiquement insensées, du genre : « π est-il un groupe ? ».

Par ailleurs, l’égalité $x=_A y$, pour deux membres $x,y$ d’un type $A$, est elle-même un nouveau type, dont les membres représentent les preuves de l’égalité entre les deux objets $x$ et $y$ de type $A$.

Un point important, sur lequel je ne peux encore que me livrer à une expérience de psittacisme, est l’introduction par Vladimir Voevodsky de l’axiome d’univalence et qui donne son sous-titre au livre dont il est question dans ce billet. En énorme, cet axiome affirme qu’une équivalence est une égalité. Un rêve pour les catégoriciens...

Le lien entre théorie des types et théorie de l’homotopie vient de ce qu’on peut interpréter un espace comme un type, ses points comme des membres de ce type, et si $p,q$ sont des points, le type $p\to q$ comme les chemins de $p$ vers $q$. Comme les chemins sont réversibles, on obtient de fait une relation d’égalité : après tout, un tel chemin témoigne de ce que les deux points sont dans la même composante connexe par arcs. Et la force de cette interprétation en théorie des types de la topologie apparaît aussitôt. Souvenons-nous que le type égalité possède un type égalité, comme n’importe quel type ; que sont ses membres ? Des homotopies entre chemins, bien sûr, et ainsi de suite à tous les étages. Autrement dit, toute l’homotopie supérieure déboule sans crier gare.

Il faut insister sur le fait que c’est une théorie de l’homotopie abstraite qui apparaît, c’est-à-dire sans qu’il soit besoin de parler d’espaces topologiques, et dont les énoncés sont plus forts que leurs compagnons en homotopie classique, même si leurs preuves peuvent en être inspirées.

Cette correspondance entre deux champs mathématiques (théorie de l’homotopie d’une part et théorie des types de l’autre) restés jusque-là étrangers l’un à l’autre est extrêmement féconde. La vision homotopique de la théorie des types apporte aux logiciens une intuition nouvelle sur la géométrie des objets représentants les preuves en théorie des types. Elle promet également de parvenir enfin à clarifier la description formelle des fondements des mathématiques et en particulier des catégories. Inversement, la retranscription en théorie des types homotopiques des résultats standard de topologie algébrique renouvelle la compréhension de la théorie de l’homotopie, suggérant parfois des démonstrations élégantes et nouvelles de ces théorèmes.

Formalisation et vérification de preuves

Dernier aspect, l’informatique. La notion de type est assez ancienne. Elle apparaît dès les Principia Mathematica de Whitehead et Russel, en lien avec les fondements des mathématiques et les premiers paradoxes logiques. On la retrouve aussi dans le $\lambda$-calcul de Church, et dans de nombreux langages de programmation. Dans les années 80, les travaux de Per Martin-Löf fournissent enfin un $\lambda$-calcul typé susceptible de servir de base à la description des fondements des mathématiques. C’est en effet une version de cette théorie qui est à la base des logiciels de vérification de preuve, tels que Coq (initialement issu du Calculus of Constructions de Thierry Coquand) qui ont récemment eu de jolis succès en permettant la vérification par Georges Gonthier et son équipe du théorème des 4 couleurs ou du théorème de Feit-Thompson, voir l’article Coq et caractères dans Images des Maths.

De fait, parallèlement à leur rédaction en anglais, presque tous les résultats de ce livre ont été rédigés dans deux logiciels, Coq déjà cité, ainsi qu’Agda.

J’en ai lu trop peu pour pouvoir en dire beaucoup plus. J’espère même ne pas avoir fait trop de contresens. J’espère surtout avoir transmis mon enthousiasme sans borne à la découverte d’un nouvel et merveilleux univers mathématique.

Post-scriptum :

Je remercie Jérôme Buzzi, Yves Cornulier, Étienne Ghys, Vincent Beck, Jérémie Le Borgne, Assia Mahboubi pour leurs commentaires sur les premières versions de ce texte.

Article édité par Étienne Ghys

Partager cet article

Pour citer cet article :

Antoine Chambert-Loir — «À la croisée des fondements des mathématiques, de l’informatique et de la topologie» — Images des Mathématiques, CNRS, 2013

Crédits image :

Image à la une - Couverture du livre, téléchargée depuis [http://homotopytypetheory.org/book/>http://hottheory.files.wordpress.com/2013/03/cover-web.png]

Commentaire sur l'article

  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 7 décembre 2013 à 16:12, par François Loeser

    Une coquille semble-t-il : au lieu de « Le formalisme de la théorie des types constitue une alternative à la théorie des types » il faut lire « Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles »

    Répondre à ce message
    • Une coquille...

      le 7 décembre 2013 à 21:56, par Antoine Chambert-Loir

      Bien entendu, c’était une coquille... j’en suis désolé !

      Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 7 décembre 2013 à 16:21, par Julien Puydt

    Si je puis me permettre : « Le formalisme de la théorie des types constitue une alternative à la théorie des types pour décrire les fondements des mathématiques. » devrait plutôt être : « Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles pour décrire les fondements des mathématiques. »

    Répondre à ce message
    • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

      le 7 décembre 2013 à 21:56, par Antoine Chambert-Loir

      Oui, merci !

      Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 9 décembre 2013 à 13:32, par Pierre Lecomte

    Merci d’avoir attiré l’attention sur ce livre, par votre bel et clair article !

    Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 9 décembre 2013 à 15:18, par Claude Animo

    Une remarque concernant les preuves automatiques et votre commentaire louangeur concernant « des logiciels de vérification de preuve, tels que Coq (initialement issu du Calculus of Constructions de Thierry Coquand) qui ont récemment eu de jolis succès en permettant la vérification par Georges Gonthier et son équipe du théorème des 4 couleurs ou du théorème de Feit-Thompson » :

    . combien de pages pour ces démonstration ?

    . sont-elles lisibles ? combien de millions d’inférences ?

    . qui peut les relire.

    . qui a démontré le démonstrateur ? lui-même ? un autre ?

    En conclusion, peut-on encore parler de démonstrations donc de preuves ?

    Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 10 décembre 2013 à 00:08, par Antoine Chambert-Loir

    Je n’ai pas regardé les vérifications de l’équipe de Gonthier, mais j’avais jeté un œil au livre de Thomas Hales (Dense sphere packings — A blueprint for formal proofs), qui est assez lisible (c’est, si je puis dire, une traduction en langage usuel de la preuve formelle). De fait, ainsi qu’explique Hales (par exemple dans son article « Mathematics in the Age of the Turing Machine »), les preuves formalisées ne sont guère plus longues que les preuves originelles.)

    Enfin, les logiciels de vérifications de preuves ont un noyau initial très petit qu’on peut vérifier facilement, et le reste est fait de proche en proche (un peu comme les compilateurs des langages modernes).

    Enfin, entre des dizaines de pages d’études de cas, et une description formelle des calculs qu’il faut mener, jointe au résultat de leur vérification mécanisée, je vous laisse juge de ce qui est le plus sûr.

    Toutefois, vérifier informatiquement une preuve n’améliore a priori pas la compréhension des mathématiques (à moins que pour ne faire cette vérification, on n’ait été amené à penser différemment la preuve que l’on vérifie). Cette dernière assertion doit être bémolisée : dans le livre dont cette chronique est l’objet, de nombreuses preuves ont d’abord été menées à l’aide du logiciel de vérification de preuve (qui mérite dans ce cas son nom d’« assistant de preuves »).

    Répondre à ce message
    • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

      le 10 décembre 2013 à 13:45, par Claude Animo

      « Toutefois, vérifier informatiquement une preuve n’améliore a priori pas la compréhension des mathématiques (à moins que pour ne faire cette vérification, on n’ait été amené à penser différemment la preuve que l’on vérifie). »

      Dès lors qu’une démonstration automatique échoue à se terminer (critère subjectif), il est possible d’affirmer, après s’être imprégné du déroulé partiel de la preuve, que son aboutissement nécessitera une meilleure compréhension des mathématiques mises en jeu (création de nouveaux objets et structures ?) pour parvenir à casser (divide and conquer) la complexité irréductible du processus en utilisant un autre schéma de démonstration (démontrer par exemple le lemme ad hoc au moment opportun).

      C’est en dessinant en creux nos difficultés à aboutir, que la preuve automatique, peut, me semble-t-il, éventuellement s’avérer utile.

      J’ajouterais enfin que le travail le plus important consiste à « axiomatiser » la preuve et ce travail accompli, on constatera souvent que la démonstration est alors pratiquement réalisée (j’exagère un peu).

      Merci en tout cas pour ce « hors piste » roboratif et plein d’énergie.

      Répondre à ce message
      • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

        le 17 décembre 2013 à 10:53, par Jérôme Germoni

        Attention, il n’est pas question de « preuve automatique » dans toutes ces affaires mais de « preuve formelle ». L’assistant de preuve ne produit pas une preuve à partir de rien : il certifie la validité d’une preuve qui a déjà été produite (par un humain) et qui est traduite (par un humain) dans un langage qu’il comprend. Une preuve formelle est composée d’une part de la traduction d’une preuve (qui devient un objet mathématique à part entière grâce à la théorie des types et pas un discours humain) et d’autre part d’un certificat de ladite preuve.

        Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 11 décembre 2013 à 17:46, par électron

    On peut signaler aussi que la théorie des catégories, qui est très générique, trouve des applications dans d’autres domaines tels que la linguistique (grammaires catégorielles) et la physique. Un formalisme simple permet déjà d’effectuer des traitements sophistiqués.

    Olivier

    Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 21 décembre 2013 à 21:19, par Anthony Bordg

    Merci à Antoine Chambert-Loir pour cette très bonne introduction. Je me permets d’ajouter pour répondre à certaines inquiétudes que l’avantage de la théorie des types et en particulier de la théorie des types avec l’axiome d’univalence est qu’elle permet des preuves formelles qui sont de tailles tout à fait comparables aux preuves informelles (évidemment des preuves informelles comme dans la pratique courante des mathématiciens sont aussi possibles, c’est d’ailleurs le choix de présentation du livre mentionné) et qui restent relativement compréhensibles. Evidemment rien n’interdit en théorie des ensembles, disons ZFC, des preuves formelles mais celles-ci deviennent vite incompréhensibles même aux mathématiciens chevronnés et sont d’une complexité qui explose très vite. Cette mise au pas de la formalisation et l’absence d’énoncés
    sans sens sont donc deux avantages des fondations univalentes qui ressortent bien de l’article de monsieur Chambert-Loir.

    Répondre à ce message
    • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

      le 26 mai à 21:24, par Boule Chevelue

      Bonjour,

      Quand vous dites : « l’avantage de la théorie des types et en particulier de la théorie des types avec l’axiome d’univalence est qu’elle permet des preuves formelles qui sont de tailles tout à fait comparables aux preuves informelles » et : « Evidemment rien n’interdit en théorie des ensembles, disons ZFC, des preuves formelles mais celles-ci deviennent vite incompréhensibles même aux mathématiciens chevronnés et sont d’une complexité qui explose très vite », s’agit-il d’observations empiriques ou existe-il des résultats précis sur les complexités de ces différentes preuves ?

      Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 16 avril 2014 à 09:40, par Jérôme Germoni

    Le séminaire Bourbaki de juin 2014 met la théorie homotopique des types et la preuve formelle au programme : un exposé de Thierry Coquand sur Théorie des types dépendants et axiome d’univalence et un de Thomas Hales sur Developments in formal proofs.

    Répondre à ce message

Laisser un commentaire

Forum sur abonnement

Pour participer à ce forum, vous devez vous enregistrer au préalable. Merci d’indiquer ci-dessous l’identifiant personnel qui vous a été fourni. Si vous n’êtes pas enregistré, vous devez vous inscrire.

Connexions’inscriremot de passe oublié ?

Suivre IDM