Le tableau et l’ordinateur

Au cours de la deuxième moitié du XXe siècle, l’usage d’ordinateurs de plus en plus puissants s’est rapidement répandu dans les laboratoires de mathématiques, transformant le quotidien des chercheurs. La rapidité des échanges d’idées, la typographie des documents mathématiques, et bien sûr, la puissance de calcul des machines et les logiciels qui l’exploitent, ont profondément modifié l’activité de recherche en mathématiques. L’ordinateur a ainsi permis de résoudre des conjectures anciennes et même suscité des formes nouvelles de mathématiques.

Un instantané de tableau noir

Pourtant, demandez à un mathématicien quel est l’objet le plus important de son bureau, et il y a de grandes chances qu’il vous réponde que c’est son tableau, et les craies qui vont avec. En effet, c’est là l’instrument irremplaçable de la partie la plus créative de l’activité mathématique : comprendre l’essence d’une démonstration, d’une définition, expliquer ou explorer des idées nouvelles. Au cours de la dernière décennie, l’ordinateur a néanmoins ajouté une nouvelle corde à son arc, et propose désormais aux mathématiciens des outils informatiques pour les assister dans la vérification des démonstrations mathématiques.

En 2006, Benjamin Werner écrivait pour Images des Maths un article intitulé La vérité et la Machine à l’occasion de son travail avec Georges Gonthier sur la vérification du théorème des quatre couleurs. Cet article mentionne déjà le travail initié par Thomas C. Hales sur la vérification de sa preuve de la conjecture de Kepler [1]. À cette date, les outils informatiques de vérification de preuves étaient surtout connus pour leurs applications au problème de la preuve de propriétés de programmes et Thomas C. Hales est l’un des premiers à vouloir appliquer ces techniques à des résultats issus de sa propre recherche en mathématiques et reposant sur des calculs, mais pas que. Depuis le cercle des chercheurs qui s’intéressent aux progrès de ce domaine s’est encore élargi, et les motivations qui les animent dépassent largement le cadre des preuves calculatoires. Vladimir Voevodsky, médaille Fields en 2002, explique ainsi dans un récent exposé à destination du grand public et donné à l’Institute for Advanced Study de Princeton comment ses doutes croissants sur la fiabilité de ses propres résultats l’ont poussé vers l’étude des fondements des mathématiques et des preuves vérifiées par un ordinateur. Pourtant, ses domaines de prédilection ne sont pas de ceux qui reposent de façon cruciale sur une puissance de calcul surhumaine. Simultanément, les outils qui permettent de conduire ces vérifications ont atteint une maturité suffisante pour traiter des résultats significatifs et contemporains. Par exemple une équipe menée par Georges Gonthier a achevé en 2012 une vérification complète à l’aide de l’assistant de preuve Coq d’un résultat complexe de théorie des groupes finis appelé théorème de l’ordre impair et établi en 1963 par Walter Feit et John G. Thompson. Ce travail a également fait l’objet d’un article des Échos de la recherche, Coq et caractères, par Jérôme Germoni.

Anatomie d’un assistant de preuve

Utiliser une machine pour vérifier des démonstrations mathématiques n’est pas une idée nouvelle, loin s’en faut. Par exemple, on peut admirer au musée de l’histoire des sciences d’Oxford le beau Piano Logique conçu par William Stanley Jevons qui date de la fin du XIXe siècle.

Les touches du piano logique de W. S. Jevons

Aujourd’hui, l’ordinateur a remplacé ces machines mécaniques et pour vérifier automatiquement une démonstration, on utilise un logiciel appelé assistant de preuve. Tout comme il existe une variété de logiciels disponibles pour faire des calculs ou mettre en forme des textes, il existe de même plusieurs assistants de preuve. Ces logiciels proposent un environnement de travail qui permet de décrire de façon formelle des énoncés mathématiques, des démonstrations ainsi que de vérifier automatiquement leur correction. Il est important de noter ici que c’est bien la vérification des preuves qui est automatique, et non leur découverte : l’utilisateur doit bel et bien fournir une description non seulement de l’énoncé à valider mais aussi de la démonstration candidate — c’est ce qu’on appelle formaliser une démonstration.

Le schéma ci-dessous illustre les composants principaux d’un assistant de preuve.

Squelette d’un assistant de preuve

Pour construire un assistant de preuve, il faut d’abord se donner un langage formel, qui est un formalisme logique. Ce composant codifie l’écriture formelle des énoncés mathématiques et des démonstrations. Il définit les règles de bonne formation des
démonstrations, et permet de réduire la vérification des preuves à un procédé
mécanique. Cette tâche peut par suite être confiée à un
programme appelé le noyau. Celui-ci est vraiment la clef de voûte de
l’assistant de preuve : ce sont ces mêmes quelques lignes de
programme qui vont valider toutes les démonstrations soumises par
l’utilisateur. Ainsi, si l’on est convaincu que ce programme est un
vérificateur de preuves fiable, on pourra faire confiance à toutes les
démonstrations qu’il valide. Autrement dit, la vérification d’une
preuve mathématique arbitraire est ramenée à la confiance en la
correction d’un programme unique qui sait les vérifier toutes.
C’est pourquoi ce composant doit rester simple et sans optimisation
excessive.

L’étagère formalisée dans la version digitale du théorème de l’ordre impair

Maintenant que l’on a fixé un langage formel pour écrire les énoncés et
leurs preuves, il s’agit de décrire concrètement les
théories qui nous intéressent dans ce langage et d’utiliser le noyau
pour en vérifier les démonstrations. C’est ici que s’exerce la
créativité de celui qui écrit les bibliothèques formelles, qui doit
trouver la définition adéquate des objets mathématiques à un niveau de
détail souvent absent de la littérature. À ce stade on se heurte
également au fossé qui sépare le
langage avec lequel les mathématiciens communiquent de façon
intelligible et la verbosité exigée par une telle vérification
exhaustive. En effet l’intelligibilité du discours des mathématiciens requiert un appareil d’abstraction, conventions et notations sans
lequel le propos est enseveli sous les détails. Ce contenu implicite
doit néanmoins être restauré pour que le vérificateur de preuve, que
l’on veut simple, impitoyable, et donc stupide, puisse valider la
preuve. Transcrire complètement dans le langage verbeux de la logique des mathématiques contemporaines semblait un impossible grand écart aux mathématiciens du collectif Nicolas Bourbaki, qui repoussent à plusieurs reprises dans leurs écrits la faisabilité, sinon l’intérêt même d’une telle entreprise [2]. Mais le développement postérieur des preuves
formelles assistées par ordinateur apporte un éclairage différent.

De fait, pour que l’activité de formalisation reste possible malgré ce
grand écart, un assistant de preuve fournit à son utilisateur une
panoplie d’outils qui permettent de minimiser l’information que l’on
doit fournir pour décrire sa preuve candidate. Ces outils jouent par
exemple le rôle de l’entraînement souvent quasi-inconscient du lecteur
cultivé d’un texte mathématique, lorsqu’il reconstruit par lui-même ce qui
n’est pas écrit. Nul besoin d’avoir une
confiance absolue dans les outils qui permettent cette reconstruction :
tous les coups sont permis puisque in fine chaque étape de la preuve est
impitoyablement vérifiée par le noyau. Il est donc
possible ici d’utiliser toutes les heuristiques, optimisations,
automatisations que l’on souhaite pour faciliter la tâche de
l’utilisateur.

Enfin, il ne s’agit pas de
réinventer la roue chaque fois qu’une nouvelle démonstration vient à
être vérifiée : il est primordial que l’utilisateur puisse s’appuyer
sur des bibliothèques de mathématiques déjà formalisées et validées,
pour construire de nouveaux développements. Ainsi la motivation de
l’équipe qui a travaillé sur la formalisation de la preuve du théorème
de l’ordre impair n’était pas de traquer les erreurs potentielles dans
la preuve de ce résultat, mais plutôt de comprendre comment construire
une bibliothèque d’algèbre formalisée conséquente et réutilisable et
de représenter formellement toutes les mathématiques qui interviennent dans
ce résultat. Ainsi, si les chercheurs impliqués dans ce
projet n’ont pas inventé de résultats mathématiques nouveaux, ils ont
dû réfléchir à la meilleure représentation formelle de pans variés de
mathématiques et organiser ces théories de façon à assurer la
cohésion de tout l’édifice.

Chacun sa logique

La grande diversité des assistants de preuve tient en partie au
choix que chacun d’entre eux fait pour la logique qui le sous-tend. Il
y a de multiples choix possibles pour ces fondements, qui
influent de façon significative sur l’activité de formalisation.
La première qualité que l’on demande à un tel formalisme logique est sa
cohérence : il est indispensable de s’assurer que le cadre de
départ dans lequel on va travailler est non contradictoire pour avoir
confiance dans les preuves que l’on va formaliser !

En fait, cette preuve de non contradiction ne peut pas être exprimée dans le formalisme lui-même si celui-ci est suffisamment expressif pour nos besoins : c’est l’essence du second théorème de Gödel [3]. Mais on peut tout à fait faire une preuve de non contradiction, en la formalisant dans une logique légèrement plus puissante. Une autre possibilité consiste à traduire le formalisme qui nous intéresse dans un autre, considéré comme mieux compris, comme la théorie des ensembles de Zermelo-Fraenkel. Idéalement cette étude de la cohérence doit être elle-même vérifiée par l’assistant de preuve lui-même. C’est chose faite pour la plupart des assistants de preuve. Il reste ensuite à se convaincre que le vérificateur de preuves que l’on programme pour ce
formalisme logique n’a pas de bugs. Le plus souvent, la taille de ce vérificateur est suffisamment petite pour qu’une inspection manuelle soit réaliste. Mais il est possible d’aller plus loin et d’utiliser toute la panoplie des méthodes formelles qui garantissent non seulement la preuve mathématique que les spécifications du programmes sont respectées, mais aussi que son exécution est fiable, en tenant compte d’aspect de plus bas niveau comme la gestion de la mémoire, de la compilation, etc.

À l’autre extrémité de la chaîne, le choix du formalisme sous-jacent aura des conséquences sur la façon dont on exprimera les définitions des objets mathématiques et leur propriétés. Par exemple, dans les formules mathématiques, on utilise traditionnellement des notations concises appelées quantificateurs pour indiquer la portée de la propriété que l’on énonce. Mais pour préciser le formalisme logique avec lequel on veut travailler, il est nécessaire d’expliquer dans la syntaxe formelle sur quelle nature d’objets on aura le droit de faire porter nos quantifications : certains formalismes interdisent ainsi de faire porter les quantificateurs sur des objets trop compliqués, comme les fonctions. Par exemple dans ce cas, pour exprimer que tout polynôme non nul à coefficients dans un certain corps $K$ a au moins une racine, on écrira la chose suivante :
\[ \forall p_0,\dots,p_{n +1} \in K, p_{n+1} \neq 0 \Rightarrow \exists x \in K, p_{n+1}x^{n+1} + \dots + p_0 = 0 \]
qui est une famille de formules paramétrée par un entier $n$. En effet on ne dispose pas dans cette syntaxe bridée, dite du premier ordre, de l’expressivité suffisante pour donner un sens aux points de suspension, c’est à dire pour faire varier arbitrairement, mais dans une seule et même phrase, le nombre de quantificateurs
$\forall $ qui permettent de parler d’un polynôme arbitraire. Par contre, si on autorise la quantification à porter sur des fonctions, la même notion s’écrira plutôt :
\[ \forall P \in K[X], \textrm{deg}(P) > 0 \Rightarrow \exists x \in K, P(x) = 0 \]
qui est une unique formule. On parle alors de logique d’ordre supérieur.
Ce petit exemple illustre combien la description des structures mathématiques et de leur théorie se trouve affectée par l’expressivité du formalisme choisi.

Note : ceci implique que vous ne devez pas klaxonner pour la seule raison que je laisse traverser un piéton et que vous êtes derrière moi (xkcd)

Les différentes natures de quantifications ne sont pas les seuls
paramètres dans le choix du formalisme, loin s’en faut [4], et dans toute
sa généralité cette question d’expressivité a une importance toute
particulière. Très grossièrement, plus un formalisme logique est rudimentaire, plus ses propriétés (méta)mathématiques comme sa cohérence, son expressivité, etc. sont faciles à étudier. Si une large part des mathématiques est en théorie exprimable dans une logique très élémentaire, se contraindre en pratique à une logique minimale n’est pas forcément pertinent dans notre
contexte. L’une des difficultés principales de l’exercice de formalisation est la
(re)définition formelle de tous les objets mathématiques qui composent
la théorie étudiée. En particulier, il faut se convaincre que l’objet ou l’énoncé avec lequel on travaille dans la preuve formelle est le reflet fidèle de celui qui est décrit dans la littérature de référence. Cette vérification, qui celle-là ne peut être qu’humaine, peut être rendue beaucoup plus difficile lorsqu’un langage trop pauvre obscurcit le propos en imposant trop de codages et d’annotations.

Ainsi, le choix d’un bon formalisme pour fonder un assistant de preuve est essentiellement guidé par deux critères parfois en tension : l’aisance avec laquelle on pourra concevoir un vérificateur de confiance pour ce formalisme et le confort avec lequel on pourra y exprimer les mathématiques qui nous intéressent. Il n’y a pas de « meilleure logique possible », mais des compromis fondés sur l’usage auquel ses concepteurs destinent l’assistant de preuve a priori, qui peut aller de la vérification des propriétés de circuits logiques à la formalisation de pans d’algèbre abstraite, d’où la variété des outils disponibles.

Une grande famille d’assistants de preuve est fondée sur une variante
de ce que l’on appelle la théorie des types, formalisme alternatif à la célèbre théorie des ensembles. C’est en particulier le cas des
assistants de preuve utilisés ou étudiés par les deux orateurs du séminaire
de ce mois. Dans le reste de cet article, nous essaierons de donner une idée de l’esprit de ce formalisme et de la façon dont on peut l’utiliser pour fonder un assistant de preuve. Nous partirons d’une définition formelle de la notion de fonction, de la façon dont on peut décorer les fonctions avec des types, pour s’apercevoir que nous faisions de la logique sans nous en douter.

À l’origine sont les fonctions

Mais avant de parler de types, il nous faut parler fonctions. En effet, à la base de la théorie des types se trouve une définition formelle de la notion de fonction, appelée $\lambda$-calcul. Inventé par le mathématicien Alonzo Church, le $\lambda$-calcul est un système formel en apparence très élémentaire [5].

Pour commencer, considérons une collection $V$ de symboles, assez grande pour nous permettre de piocher dedans autant de symboles distincts qu’il nous plaira [6]. En $\lambda$-calcul, on ne sait parler que de trois natures d’objets, que l’on nomme les termes du $\lambda$-calcul.
Les termes les plus simples sont les éléments de $V$ : un élément $x\in V$ est appelé une variable. Puis, si nous disposons de deux termes $t_1$ et $t_2$ préalablement construits, on peut former le nouveau terme $t_1(t_2)$ qui s’appelle l’application de $t_1$ à $t_2$. Intuitivement, on voit $t_1$ comme une fonction, appliquée à $t_2$, son argument. Enfin, si nous disposons d’une variable $x$ et d’un terme $t$, on peut former un nouveau terme $(\textrm{fun}\ x \mapsto t)$ : la fonction qui à $x$ associe $t$. En fait le terme $(\textrm{fun}\ x \mapsto t)$ est traditionnellement notée $\lambda x. t$ dans ce contexte, suivant la notation historique introduite par Church et qui donne son nom au système formel.

Par exemple, le terme $(\textrm{fun}\ x \mapsto x)$ représente la
fonction identité, de même que le terme $(\textrm{fun}\ y \mapsto y)$
car les variables $x$ et $y$ sont muettes (on dit aussi « liées »). Le terme
$(\textrm{fun}\ x \mapsto y)$ représente quant à lui la fonction constante qui vaut $y$, un paramètre de cette définition, quel que soit l’argument fourni. Le terme $(\textrm{fun}\ f \mapsto (\textrm{fun}\ x \mapsto f(x)))$ représente
la fonction à deux arguments qui applique son premier argument à son
second tandis que le terme $(\textrm{fun}\ x \mapsto x(x))$ représente
la fonction qui applique son unique argument à lui même. Que se
passe-t-il lorsqu’on applique une fonction à un argument ? On s’attend
à ce qu’un calcul se passe, qui produise la valeur de la fonction en
ce point. Ce calcul est modélisé par une règle de réécriture appelée réduction.

Par exemple le terme $(\textrm{fun}\ x \mapsto x)(y)$, l’identité
appliqué à $y$, se réduit vers le terme $y$ : la valeur de la fonction
identité en $y$ est bien $y$. Ce système formel est un outil
extraordinairement puissant pour l’étude théorique de la
calculabilité
 [7]
et des langages de programmation et fait encore aujourd’hui l’objet
d’une recherche active.

Les termes du $\lambda$-calcul munis de leur règle de réduction
modélisent en fait la notion même de calculabilité, et la motivation
de Church n’était autre que de donner une définition formelle de ce concept. Le $\lambda$-calcul est ainsi exactement
aussi expressif qu’un autre modèle de calcul bien connu, celui des
machines de Turing [8]. On peut de fait aussi modéliser par un $\lambda$-terme des calculs qui ne rendent jamais de résultat car ils ne terminent pas : prenons par exemple le terme $(\textrm{fun}\ x \mapsto x(x))$ que nous avons déjà rencontré, et
appliquons le à lui même :
\[(\textrm{fun}\ x \mapsto x(x))\ (\textrm{fun}\ x \mapsto x(x))\]
Ce terme, souvent appelé $\Omega$, a la forme d’une fonction appliquée à un argument, on peut donc effectuer une réduction. Mais celle-ci va transformer le terme en ... lui-même.

Théorie des Types

Bertrand Russell en 1936

Il existe des variantes de $\lambda$-calcul qui permettent de filtrer certains termes considérés comme pathologiques par un procédé syntaxique basé sur un jeu d’étiquettes appelés types. Le premier usage de cette idée semble être
dû à Bertrand Russell (encore lui [9]), qui les introduit dès le début du XXe siècle pour stratifier les énoncés logiques et éviter les phénomènes d’auto-référencement du type paradoxe du menteur.

Si l’usage de ces types trouvent leur origine dans les travaux liés aux fondements des mathématiques, ils sont pourtant peu à peu oubliés par la littérature mathématique dès le milieu du XXe siècle et c’est en fait dans le domaine alors émergeant de la théorie des langages de programmation que l’usage des types a finalement été le plus répandu : dans certains langages il est possible de prescrire le type des arguments d’un programme ainsi que son type de retour pour éviter de déclencher des comportements non voulus et imprévisibles. Par exemple, un
programme qui attend un entier ne s’exécutera pas si on lui fournit un tableau en argument.

Revenons au $\lambda$-calcul : nous allons rendre notre système formel un peu plus sophistiqué. Par exemple lorsque tout à l’heure nous avons dit que le terme \[(\textrm{fun}\ x \mapsto x)\] représentait la fonction identité, nous allons maintenant attribuer une étiquette à cette fonction pour décrire le lieu de ses arguments et celui de ses valeurs. Par exemple,
\[ f := (\textrm{fun}\ x \mapsto x)\ : \mathbb{N} \rightarrow \mathbb{N}\]
est la fonction identité étiquetée par $\mathbb{N} \rightarrow \mathbb{N}$ et il s’agit de l’identité sur $\mathbb{N}$, tandis que
\[g := (\textrm{fun}\ x \mapsto x)\ : (\mathbb{N} \rightarrow \mathbb{N}) \rightarrow (\mathbb{N} \rightarrow \mathbb{N})\]
est l’identité sur les fonctions à une variable dans $\mathbb{N}$ et à valeurs dans $\mathbb{N}$. Une fonction va avec son type, $f$ et $g$ sont donc des objets distincts. Appliquer $g$ à un entier n’a pas de sens et sera donc interdit par notre système formel.
Ainsi en plus des termes du $\lambda$-calcul présenté plus haut, nous nous donnons aussi un ensemble d’étiquettes, appelées types, et des règles qui expliquent
sous quelles conditions on a le droit de coller une étiquette donnée à un terme donné.
Notre type le plus simple est un symbole, que nous noterons $\omicron$, et qui joue le rôle du $\mathbb{N}$ de nos exemples précédents. On peut aussi construire récursivement de nouveaux types en mettant des flèches entre deux types arbitraires déjà construits : par exemple $\omicron \rightarrow \omicron$ ou $(\omicron \rightarrow \omicron) \rightarrow (\omicron \rightarrow \omicron)$ sont des types. Si $A$ et $B$ sont de tels types, alors $A \rightarrow B$ est le type des fonctions dont l’argument a le type $A$, et qui calculent un résultat de type $B$. Par exemple, on peut attribuer au terme $(\textrm{fun}\ x \mapsto x)$ le type
$\omicron \rightarrow \omicron$ et on parle alors de la fonction identité sur les objets de type $\omicron$. De plus alors que dans notre première version du $\lambda$-calcul, on pouvait former l’application $t_1(t_2)$ de n’importe quelle fonction $t_1$ à n’importe quel argument $t_2$, on ne s’autorise désormais des termes de la forme $t_1 ( t_2)$ que si $t_1$ a un type de la forme $A \rightarrow B$, c’est à dire une fonction, et $t_2$ le type $A$, c’est à dire un argument du bon type.

Dans le contexte d’un langage de programmation, nous avons vu que l’utilisation des types permettait de détecter rapidement certaines erreurs en vérifiant que les spécifications prescrites dans les types sont respectées. Cette possibilité de filtrer certaines phrases considérées comme dénuées de sens est également intéressante lorsque l’on vérifie des mathématiques avec un ordinateur. Non seulement cette vérification est plus aisée mais l’écriture des énoncés mathématiques formalisés est aussi plus facile. En effet grâce au typage on peut dispenser l’utilisateur d’une partie des annotations de bas niveau et programmer leur inférence automatique.
C’est au début des années 70, que Robin Milner conçoit le langage
de programmation ML, mettant en pratique les avancées récentes dans la compréhension des systèmes de types.

Robin Milner, lauréat du prix Turing en 1991, travaillant au tableau

Une de ses motivations principales était de se doter d’un bon langage pour développer l’un des premiers logiciels de démonstration
formelle, appelé LCF (pour Logic of Computable Functions), qui est un autre de ses sujets de recherche. Ces travaux précurseurs ont jeté les bases de toute une famille de langages de programmation modernes comme le langage Ocaml développé en France par l’Inria. Ce sont les mêmes travaux qui ont posé les principes toujours actuels de la conception des assistants de preuve. Le système HOL-Light utilisé par Thomas Hales dans ses travaux sur la conjecture de Kepler en est un héritier direct.

La logique dans tout ça

Voici comment un logicien écrit de façon formelle la règle qui régit la concordance entre le type d’une fonction et de l’argument auquel elle s’applique :
\[ \frac{ t_1 : {\color{red} {A \rightarrow B}} \quad t_2 : {\color{red}A}} { t_1 (t_2) : {\color{red}B}} \]
Cette notation, appelée règle d’inférence, se lit de haut en bas, comme on pose une opération : au dessus de la barre, les hypothèses sur les types de $t_1$ et $t_2$, en bas la conclusion sur le type de $t_1 (t_2)$. Pour donner la définition complète de notre système formel, il faudrait aussi écrire deux autres règles d’inférences, pour expliquer comment sont typées les variables et les fonctions, mais nous éviterons de rentrer dans ces technicités. En effet la version colorée de cette seule règle fait déjà apparaître un phénomène remarquable. Fermons ainsi les yeux sur les termes (en noir) pour ne regarder que leurs étiquettes (en rouge). Alors, on peut lire ce qu’on appelle le modus ponens, c’est à dire la règle qui explique comment utiliser une implication dans un discours logique : si on démontre une implication d’une part, et sa prémisse d’autre part, on aura établi la conclusion de l’implication. Pour passer des types aux propositions logiques, il suffit de remplacer mentalement la simple flèche
$\rightarrow$ par une « double » flèche $\Rightarrow$. Réciproquement, en partant d’un énoncé logique propositionnel $P$ dont les seuls connecteurs sont des implications, on obtient un type $T_P$ en changeant les $\Rightarrow$ pour des
$\rightarrow$. Le résultat important est que la formule $P$ de départ est démontrable si et seulement si il existe un terme $t$ du $\lambda$-calcul qui a le type $T_P$.

L’idée importante ici est que l’on peut lire certains types du $\lambda$-calcul comme des propositions, des énoncés logiques, et interpréter les termes ayant un tel type comme une représentation formelle des preuves de cet énoncé. Par exemple pour représenter l’énoncé « Faux », on pourra se donner une constante de type qui par définition n’étiquette aucun terme. Avec la version simple de $\lambda$-calcul que nous avons décrit, appelé $\lambda$-calcul simplement typé, on ne peut modéliser que des énoncés très simples, ceux de la logique propositionnelle. Mais il est possible d’enrichir le système de types avec lequel on travaille pour pouvoir parler de plus de connecteurs logiques. Par exemple, on pourra considérer des types dépendants de termes pour modéliser des prédicats. On verra ainsi le prédicat « être premier » comme une fonction des nombres entiers vers les propositions, donc un objet de type $\mathbb{N} \rightarrow \iota$ si on note $\mathbb{N}$ le type des entiers et $\iota$ celui des propositions. Un énoncé universellement quantifié sur les éléments d’un type $C$ est représenté par une famille, indexée par les termes de type $C$, de types
$P : C \rightarrow \iota$ dépendant d’un terme de type $C$. On note cette famille $\forall x : C, P (x)$. La règle de typage associée à cette nouvelle construction de types ressemble étrangement à celle que nous avons étudiée pour le cas des fonctions, et c’en est de fait une généralisation :
\[ \frac{ t_1 : {\color{red} {\forall x : C, P(x)}} \quad t_2 : {\color{red}C}} { t_1 (t_2) : {\color{red}P(t_2)}} \]
Les objets du type $\forall x : C, P(x)$ sont précisément des fonctions
$(\textrm{fun } x \mapsto t)$ dont l’argument $x$ est de type $C$ et le corps $t$ a le type $P(x)$. Par exemple, si $P(x)$ est le type des nombres premiers plus petits que l’entier $x$, on pourra donner le type $\forall x : \mathbb{N}, P(x)$ à une fonction qui calcule le plus grand diviseur premier d’un entier. On voit ici que ces nouvelles constructions de typage, types dépendants de termes, et familles indexées ont fait faire un grand bond dans l’expressivité de notre système formel. Avec le $\lambda$-calcul simplement typé, on vérifiait la bonne formation de l’application des fonctions à leurs arguments. En autorisant des types dépendants, on peut aussi préciser dans le type d’une fonction les propriétés attendues sur le résultat qu’elle calcule. Remarquons aussi qu’avec le $\lambda$-calcul simplement typé, on pouvait reconnaître des énoncés logiques de la logique propositionnelle implicative, avec ces nouvelles constructions, on est entré dans la logique d’ordre supérieure.

Des fonctions et des preuves, des énoncés et des types

Ces exemples esquissent une correspondance précise qui relie les énoncés logiques avec des types et leur démonstrations avec des fonctions. On peut la comprendre en voyant les termes, en noir, de nos règles comme des descriptions
des démonstrations des énoncés en rouge qui les typent. Ainsi, la preuve d’une
implication $C \Rightarrow B$ est ici décrite comme une fonction
qui, étant donné une preuve arbitraire de $C$ permet de construire une
preuve valable de $B$. Mais la preuve d’un énoncé universel
$\forall x : C, P(x)$ est aussi une fonction, qui étant donné un élément $c$ quelconque du type $C$ construit une preuve de l’instance $P(c)$. On peut étendre le $\lambda$-calcul typé pour travailler avec des formalismes beaucoup plus expressifs tout en maintenant cette correspondance [13].

Pour construire un formalisme logique et un vérificateur de preuve à
partir d’une théorie des types, on commence par identifier certains
types avec des énoncés logiques. Dans notre exemple, nous avons ainsi
par exemple identifié une implication $A \Rightarrow B$ avec le type $A \rightarrow B$ de certaines fonctions. Avec un système formel
plus sophistiqué, il existe des types qui modélisent une formule
logique arbitrairement complexe, utilisant des conjonctions, disjonctions, quantificateurs... Pour promouvoir cet énoncé au statut de théorème, il faut exhiber un terme qui a ce type, et vérifier qu’il existe une séquence (en fait un arbre) de règles de typage qui le justifie. C’est là le principe à la base des assistants de preuve fondés sur la théorie des types : l’utilisateur construit des termes et le vérificateur vérifie des arbres de typage. Le programme qui implémente l’algorithme de typage est le noyau de l’assistant de preuve.

Nicolaas de Bruijn (à droite) et Bert Jutting (assis à l’ordinateur) sur le point d’achever la vérification du traité « Fondations de l’Analyse » d’Edmund Laudau et de le fêter comme il se doit.

Pour finir, insistons sur le fait que ce sont exactement les même constructions du $\lambda$-calcul qui représentent les fonctions « usuelles », par exemple des entiers vers les entiers, et les démonstrations, qui vues comme des fonctions opérant sur les preuves. Un formalisme basé sur cette correspondance a ainsi la particularité de donner une définition formelle unifiée à tous les objets mathématiques,
ceux qui nous sont familiers, comme les fonctions, mais aussi les
démonstrations des énoncés qui qualifient ces derniers.

En gommant la distinction usuelle entre deux étages de
formalisme, comme c’est en particulier le cas dans les présentations
basées sur une théorie des ensembles, on rend aux démonstrations le
statut d’objets mathématiques comme les autres. Cette uniformité est
l’un des attraits de la correspondance de Curry-Howard comme fondation
pour la conception d’un assistant de preuve. Le tout premier de ces systèmes,
appelé AUTOMATH et conçu par de Nicolaas Govert de Bruijn était d’ailleurs déjà basé sur un tel formalisme, suivi par d’autres comme les logiciels NuPRL, Coq, Agda,...

Perspectives

Ce sont les travaux du mathématicien suédois Per Martin-Löf dans les
années 80 qui ont posé les bases des théories des types plus
sophistiquées utilisées aujourd’hui dans ces outils.
Le calcul des constructions, dû à Thierry
Coquand et qui sous-tend l’assistant de preuve Coq, en est un
descendant. C’est en s’intéressant à cette famille de formalismes que
Vladimir Voevodsky a mis en lumière des correspondances inédites
entre théorie des types et théorie abstraite de l’homotopie, qui
suggèrent des intuitions nouvelles pour la compréhension de la
structure formelle des preuves d’égalité entre objets mathématiques et du formalisme catégorique [14]. Ces développements récents et abstraits
sont encore en cours d’investigation, comme le montre en particulier
l’exposé de Thierry Coquand, mais ils promettent déjà d’avoir un
impact sur la conception d’une nouvelle génération d’assistants de
preuve. Utiliser un assistant de preuve est une démarche pertinente pour vérifier une démonstration qui touche aux limites de ce que la communauté mathématique peut vérifier. Les démonstrations qui reposent sur des calculs d’envergure, comme la preuve de Thomas C. Hales de la conjecture de Képler, sont des exemples de telles preuves. On pourrait aussi considérer que la classification des groupes finis, un théorème « monstre » à la preuve composite [15], ou bien les résultats évoqués par Vladimir Voevodsky dans son exposé à l’IAS bénéficieraient d’un tel travail de formalisation. Mais surtout, au delà de la vérification pédestre des preuves, les travaux autour de la conjecture de Képler, du théorème de l’ordre impair ou du théorème des quatre couleurs montrent que la formalisation de mathématiques avec un assistant de preuve aide à retravailler les mathématiques, à réorganiser les théories, et à proposer des démonstrations alternatives plus satisfaisantes. Il est fort probable que le tableau restera encore longtemps le compagnon indispensable du chercheur en mathématiques, mais il est permis de rêver qu’un ordinateur pourra bientôt l’aider à polir ses intuitions, affiner les définitions de ses nouveaux objets d’étude, et
embellir ses démonstrations.

Fin