J’ai toujours pensé qu’il y avait trois domaines au moins qui nous permettaient dans la vie de ne pas sombrer dans le désespoir face à l’horreur des temps. Les mathématiques, l’art et l’authentique littérature. Je dis « l’authentique » afin de ne pas avoir à confondre tout ce qui se fait et surtout se vend sous la dénomination de « littérature » ; « authentique » réfère ici à un engagement, une recherche, une volonté d’approcher au plus près une essence de quelque chose que l’on peut qualifier de présence à soi-même, d’être au plus près d’un centre intérieur, ainsi que l’ont défendu maints auteurs et autrices que j’ai parfois eu la chance de rencontrer comme Lorette Nobécourt, Charles Juliet ou René Frégni, mais aussi que je n’ai jamais pu rencontrer, soit parce qu’ils appartiennent au passé comme Proust ou Stendhal, soit parce que je n’avais jamais osé, du temps de leur vivant, les aborder, comme Philippe Jaccottet. On a peur parfois d’aller sonner trop haut, on se sent trop fragile, près à déguerpir des fois qu’une réponse se fasse entendre sous la forme d’un « qui est là ? ». Deux jours dans la semaine du 10 au 16 mars passés à Paris m’ont permis de joindre ces différents domaines et cela, de manière parfois inattendue, comme si l’enchantement et l’espoir surgissaient parfois de l’imprévu, de ce que l’on n’avait pas encore construit dans sa tête.

J’ai cité en tête de mes domaines de choix les mathématiques. Cela peut en surprendre plus d’un(e). Il y faut, il est vrai, un certain entraînement pour en goûter le caractère sublime, et même encore – je veux dire même en s’y étant frotté un peu dans sa jeunesse puis dans sa carrière d’universitaire – on n’aura pas nécessairement acquis de quoi en apprécier tous les atours, je dirai même qu’on en reste toujours loin. Mais c’est cette distance qui, peut-être, justement, nous mène à cette satisfaction intime qui nous éloigne de l’obscur des temps, comme c’est – cela est mon avis et n’engage que moi – à distance que l’on apprécie le mieux la pureté et la beauté des sommets de très haute montagne (à quoi bon les gravir et encore moins les atteindre?). Les mathématiques donc. La première motivation de ce voyage à Paris étant d’aller assister à la leçon inaugurale de Thierry Coquand, qui se tenait au Collège de France (chaire Informatique et sciences numériques) et qui portait le titre « La théorie des types, de Russell aux assistants à la démonstration ».

Je ne connais pas personnellement Thierry Coquand (qui est depuis 1996 professeur à l’Université de Göteborg), je sais seulement que les travaux auxquels je me suis intéressé en tant que chercheur lui doivent beaucoup et qu’il est resté en lien avec des chercheurs et directeurs de recherche que j’ai bien connus (dont Gérard Huet, mon strict contemporain, dont il fut l’étudiant, puisqu’il passa sa thèse sous sa direction!).

La théorie des types est quelquechose qui est apparu au début du XXème siècle quand on s’est rendu compte de la confusion dans laquelle tendaient à sombrer les mathématiques à la suite des grandes découvertes et des recherches sur les fondations attachées au concept d’ensemble. Russell avait mis le doigt sur un énorme risque d’incohérence. Il était possible d’écrire un énoncé auto-référentiel du genre de ¬P(P) qui appliquait un prédicat à lui-même pour dire que, justement, il ne s’appliquait pas à lui-même ! On ne pouvait sortir de là qu’en introduisant une hiérarchie d’ordres faisant qu’un prédicat P ne pouvait pas s’appliquer à n’importe quoi et en particulier pas à lui-même, mais seulement aux objets qui se trouvaient au niveau juste inférieur à celui qu’il occupait dans la hiérarchie. A partir de là, on pouvait songer sérieusement à inscrire les mathématiques dans un formalisme logique qui en assurerait la cohérence. D’où les entreprises de formalisation logique qui ont conduit à rechercher une forme d’automatisation des preuves. Le programme d’un grand logicien belge dans les années soixante (un certain De Bruijn) ne s’appelait-il pas justement AUTOMATH ? Il ne s’agissait pas tant, en réalité, de prouver automatiquement des théorèmes que de vérifier les preuves (et donc d’envisager non pas des démonstrateurs automatiques mais des assistants à l’écriture de preuves). Huet, dont je parlais à l’instant, le premier, réalisa le système Coq qui a permis d’assurer la justesse de maints programmes informatiques fondamentaux dans les dernières décennies. On pourrait donc penser que ces travaux sont motivés principalement par des soucis d’application industrielle. Mais pas seulement. Vouloir formaliser les mathématiques dans un cadre logique, c’est nécessairement s’interroger sur la place relative occupée par les axiomes purement logiques et ceux qui ne le sont pas. Sont logiques par exemple les axiomes de l’égalité, pourquoi le sont-ils ? Parce qu’ils transcendent tout domaine particulier, qu’ils appartiennent à ce corpus de règles qui permet qu’une connaissance (pas seulement empirique) soit possible. Comme le dit Jean-Yves Girard, « la Logique est l’affirmation prométhéenne de la possibilité d’une connaissance, limitée peut-être, mais absolument irréfragable ». Parmi les axiomes logiques de l’égalité, la réflexivité (tout objet est égal à lui-même) et le principe d’indiscernabilité, postulé dès 1686 par Leibniz : deux objets sont égaux quand toutes les propriétés de l’un sont des propriétés de l’autre¹. En revanche, on utilise en mathématiques des axiomes qui ne sont pas purement logiques, cela veut dire que l’on n’est pas obligé de les accepter ! Par exemple, l’axiome du choix, l’axiome de l’infini sont propres à la théorie des ensembles. Il existe une mathématique qui les écarte, qualifiée en général d’intuitionniste, ou bien de constructiviste : elle ne fait confiance que dans ce qu’on touche vraiment, c’est-à-dire ce que l’on peut construire au moyen de procédures reconnues comme fiables. Christian Röhmer, l’actuel directeur du Collège de France qui a la lourde tâche d’accueillir les nouveaux professeurs au cours de leur leçon inaugurale, disait justement la magie – au sens propre – des mathématiques classiques : considérer qu’un objet existe non pas parce qu’on l’a construit effectivement mais simplement parce que l’on a prouvé au moyen d’axiomes qu’il n’était pas contradictoire avec le reste des énoncés. C’est donc toujours une découverte extraordinaire quand on montre qu’un théorème que l’on a jusqu’ici prouvé au moyen d’un axiome comme celui du choix en réalité n’en dépend pas ! La traduction des mathématiques dans un langage logique est justement l’un des moyens d’y parvenir, c’est ce à quoi s’est attaché Thierry Coquand. Il faut pour cela, bien évidemment, trouver la solution pour donner aux preuves une inscription formelle au sein de la théorie (et non pas les faire apparaître comme des méta-objets). Autrement dit faire en sorte que tout le formalisme « avale » l’activité mathématique : poser des axiomes, appliquer des règles, faire des preuves, donner même une écriture interne au principe d’indiscernabilité. C’est ce que permet la Théorie des Types Dépendants, issue à la fois du Calcul des Constructions inventé par Thierry Coquand il y a au moins quarante ans, et de la Théorie des Types de Per Martin-Löf, grand mathématicien suédois, développée vers la même époque. La première innovation de ces théories aura été de traiter ensemble les objets et les preuves, ici, une variable peut désigner aussi bien un objet (un élement d’un ensemble donné) qu’une preuve (d’une proposition P), et on peut quantifier sur ces variables de sorte que l’on puisse, de manière interne au formalisme, écrire des phrases comme « pour toute preuve z de A ν B etc. ».

Le principe d’indiscernabilité possède alors une expression interne dont on ne peut voir la signification qu’en introduisant un modèle de la théorie des types, c’est-à-dire en interprétant la notion d’égalité dans un autre langage, en l’occurrence un langage « topologique », c’est-à-dire qui parle d’espaces, de chemins et d’homotopies (une homotopie entre deux fonctions continues est une déformation continue qui fait passer insensiblement de l’une à l’autre). Une telle interprétation vient des travaux d’un autre mathématicien, russe celui-ci, mais émigré aux Etats-Unis, un certain Vladimir Voïevodski (né en 1966, décédé en 2017, médaille Fields en 2002²), qui a eu l’idée de voir les types comme des espaces particuliers, dits simpliciaux, ce qui permet de voir un type dépendant B(x) (ou x appartient à A) comme un « espace de fibration » c’est-à-dire intuitivement comme une sorte de liasse de feuilles (les fibres) dont chaque page est numérotée dans A. Une famille de types est un livre, en quelque sorte, dont on feuillette les pages. Et ce genre d’espace admet une notion de chemin. De telle sorte que dire que « a est égal à x » c’est dire qu’il existe dans A un chemin qui va de a à x et que a = a soit le chemin qui va de a à a (une boucle).

La chose surprenante est que la loi d’égalité (ce qu’est devenu notre principe d’indiscernabilité) se résume alors à une notion toute simple: la contractibilité : un chemin d’un point a à un point quelconque x peut toujours être déformé continûment en un chemin constant autour de a³. Ce qui est démontrable dans la théorie homotopique. Voïevodski généralise alors les notions laborieuses d’extensionalité (quand dit-on que deux ensembles sont égaux ? que deux fonctions sont égales ? Etc.) par un seul principe, dit d’univalence, lequel peut être exprimé dans un des systèmes d’assistance aux preuves comme Coq, et qui fait en sorte que de nombreux théorèmes jusque là utilisant l’axiome de choix peuvent être prouvés dans ce cadre⁴.

Voilà donc la magie des mathématiques : chercher, ne pas toujours trouver, mais quelquefois découvrir là où on ne s’y attendait pas, des voies nouvelles, jusque là insoupçonnées, et qui renouvellent pour longtemps la façon dont jusque là nous réfléchissions à certains problèmes, c’est en cela qu’elles portent la marque de l’espoir.

1 Dans certaines approches que je qualifierai de radicales (je parlais à l’instant de J.Y. Girard), ceci est contesté. Qu’entendons-nous par propriété d’un objet ? La place où il figure dans l’espace en fait-elle partie, par exemple ? Dans a = a, n’y a-t-il pas deux instances de a, l’une qui est à gauche et l’autre qui est à droite ?

2 Il avait échoué à ses études à l’université de Moscou car il avait raté ses examens de marxisme-léninisme.

3 Ceci est, paraît-il, le principe du cordon d’aspirateur… après avoir mis votre cordon dans n’importe quel état, relachez-le : il va naturellement reprendre sa place !

4 On pourra dire que ce principe d’univalence récèle en lui une forme de l’axiome de choix, mais des travaux intéressants ont prouvé que sa justification pouvait, de fait, en être indépendante.