La vérité et la machine

Du point de vue logique, une proposition peut être déclarée vraie dans un certain formalisme si elle admet une preuve formelle vérifiant les règles de ce formalisme. Un texte mathématique traditionnel peut alors être vu comme une description « informelle » de cette preuve formelle ; son but est de convaincre le lecteur mathématicien de l’existence de cette preuve. C’est ainsi qu’au cours du siècle dernier, le consensus s’est fait autour de l’idée que la vérité mathématique était une notion exacte et objective.

L’écriture mathématique de Frege (1872).

Toutefois, dans la pratique mathématique, cet objet-preuve est longtemps resté virtuel. S’il est, en principe, possible d’écrire, ou de « dessiner », une preuve entièrement formalisée, sa taille, c’est-à-dire le nombre d’étapes élémentaires de déduction, rend cette entreprise à peu près impossible en pratique, sauf si la preuve est mathématiquement triviale. Qui plus est, il est vain de croire qu’aligner des symboles peu intuitifs sur le papier réduira de quelque façon que ce soit le risque d’erreur. En d’autres termes, la logique mathématique est, au départ, une discipline fondamentale et peu applicable, néanmoins destinée à être appliquée.

L’arrivée de l’ordinateur

Si un étudiant en informatique d’aujourd’hui regarde les écrits de Frege, il ne peut être que frappé par ce qui lui apparaîtra comme la nature essentiellement informatique des notions développées. En effet, de par leur construction arborescente, les propositions et les preuves sont typiquement des structures de données que les machines savent manipuler. L’ordinateur est le candidat idéal pour construire, stocker et surtout vérifier une preuve formelle.

Remarquons à ce titre qu’il est important de distinguer les tâches de construction et de vérification de la preuve. En particulier, lors de la vérification, on ne cherche surtout pas à rendre l’ordinateur « intelligent ». Au contraire, c’est le manque d’imagination de la machine, sa précision mécanique et son strict respect des procédures, qui permettent d’accorder à une preuve vérifiée par ordinateur un grand degré de certitude. C’est évidemment le but recherché.

Chronologiquement, le premier système de traitement de preuve fut le logiciel Automath développé par l’équipe de N.G. de Bruijn dans les années 1960. On peut considérer ce pionnier comme l’ancêtre commun des systèmes de preuve actuels. La plupart sont développés en Europe ou aux États-Unis ; on peut citer parmi d’autres Coq, Isabelle et HOL (en Europe) ou PVS (aux États-Unis).

Des preuves de programmes aux preuves mathématiques

Les systèmes de preuve, comme tous les logiciels, vivent d’abord à travers l’utilisation qui en est faite. Si, à leur débuts, les textes mathématiques, on pourrait presque dire les « classiques », ont été au centre des tout premiers travaux de formalisation, en général effectués par les concepteurs mêmes, les centres d’intérêt des formalisateurs se sont un moment éloignés des mathématiques pures, en même temps que l’on découvrait un domaine d’applications privilégié des « méthodes formelles » : la preuve de propriétés de programmes informatiques.

En effet, à l’image d’un objet mathématique, un programme obéit à des règles formelles et précisément définissables. On utilise donc un raisonnement de type mathématique pour garantir que tel ou tel logiciel (par exemple destiné au tri d’un tableau) aura bien telle ou telle propriété (rendra bien le tableau trié). Malheureusement, « à mains nues » cela se révèle rapidement assez malcommode. Une telle preuve de correction peut certes faire appel à des mathématiques tout-à-fait subtiles et non-élémentaires, mais la pratique montre que raisonner à propos d’un programme se révèle alors bien souvent plus tatillon et fastidieux que de démontrer un théorème. C’est en grande partie dû au fait qu’un programme est lui-même un objet formel. Le fait qu’il soit correct « dans les grandes lignes » n’empêche pas qu’une petite erreur suffise à faire échouer le programme lorsqu’on l’exécute sur un ordinateur.

C’est pourquoi, dans le domaine de la vérification de programmes, la compréhension ou l’intuition du raisonnement est souvent moins utile que la pure rigueur. Par ailleurs, l’utilité de ses applications paraît évidente.

On comprend donc que la certification de programmes ait fait l’objet de nombreux travaux théoriques et pratiques. De ce fait, on a intégré aux systèmes de preuve les techniques et les outils permettant de raisonner à propos de ces objets particuliers que sont les programmes.

Il est d’autant plus intéressant d’observer actuellement un certain retour de l’activité de formalisation vers les mathématiques dites pures. Une première raison en est sans doute que les progrès de ces systèmes les rendent plus confortables et efficaces, et donc aussi plus intéressants pour les mathématiciens. Il semble toutefois qu’il y ait d’autres raisons plus profondes à ce mouvement, liées à la nature d’une partie des mathématiques contemporaines. C’est ce que nous allons essayer de décrire sommairement ici.

La question du calcul

Indépendamment de la question de la formalisation, le calcul informatique joue un rôle de plus en plus important dans un certain nombre de domaines mathématiques. Un exemple radical en est la question des preuves de primalité : il ne viendrait à l’idée de personne de « prouver » une proposition comme « 2^25964951 – 1 est premier » sans recourir au calcul électronique. Si l’on veut toutefois réellement en produire une preuve, la meilleure chose que l’on puisse espérer c’est de prouver que le programme utilisé établit bien la primalité. Autrement dit, si les mathématiques sont nécessaires pour prouver la correction de programmes, les programmes peuvent à leur tour intervenir dans des preuves mathématiques.

Bien sûr, la propriété de primalité est directement liée au calcul ; mais il existe aussi des théorèmes dont l’énoncé n’est pas essentiellement calculatoire et dont les seules preuves connues reposent pourtant sur des calculs importants, numériques ou symboliques. De ceux-là, le plus célèbre est sans doute le théorème des quatre couleurs. Ce dernier a été rejoint par la preuve de la conjecture de Kepler, également célèbre. De fait, à travers de tels résultats, l’ordinateur s’est invité à la table des mathématiciens et il importe de comprendre le statut des preuves qui l’utilisent.

La particularité des quatre couleurs

Le théorème des quatre couleurs dit, rappelons-le, qu’il est toujours possible de colorier une carte planaire en utilisant au plus quatre couleurs, avec une couleur par pays, de telle manière que deux pays ayant une frontière commune ne soient pas de la même couleur. En général, on commence par ramener l’énoncé à la « quatre-coloriabilité » de graphes planaires (chaque pays correspondant alors à un sommet du graphe, relié par un arc à chacun des pays qui lui sont voisins).

La suite de l’histoire est assez connue. Conjecturée en 1852, cette proposition simple et remarquablement « concrète » a défié pendant plus d’un siècle les efforts des nombreux mathématiciens, fameux ou anonymes, qui ont cherché à la démontrer. L’aura quelque peu mystérieuse de ce théorème auprès du grand public se renforçant encore lorsque la première démonstration fut annoncée en 1976, car cette dernière « faisait appel à l’ordinateur ».

Sans chercher, bien sûr, à exposer les détails de la preuve, il est intéressant de comprendre quel genre de tâche doit être dévolue à l’ordinateur. La preuve commence par restreindre le problème à une classe de graphes planaires triangulés appelés « quasi 6-connexes ». Ensuite, on se donne une liste de petits graphes particuliers appelés configurations. Dans la preuve originelle, on en comptait 1476, nombre ramené à 633 dans une preuve de 1995. On peut alors montrer que dans tout graphe triangulé et quasi 6-connexe apparaît au moins une de ces configurations ; c’est la propriété dite d’inévitabilité. Il faut noter que même si cette étape de la preuve est, pour des raisons évidentes, particulièrement fastidieuse, elle reste à la portée d’une équipe de mathématiciens. De fait, elle fut démontrée « à la main » pour la preuve de 1976.

On raisonne ensuite par récurrence sur le nombre de sommets du graphe. En se donnant un graphe triangulé et quasi 6-connexe, on sait donc qu’il contient une configuration. On peut alors « ôter » cette configuration (en fait, la remplacer par un sous-graphe plus petit) et 4-colorier le graphe obtenu par hypothèse de récurrence. Pour conclure, il resterait alors à étendre ce coloriage du reste de la carte à la configuration. Las, il n’est en général pas possible de trouver un coloriage de la configuration qui corresponde au coloriage du reste de la carte.

C’est là qu’intervient l’explosion combinatoire de la preuve : en analysant, pour chaque configuration, l’ensemble de tous les coloriages possibles, on arrive à montrer qu’il est toujours possible de réorganiser le coloriage du reste de la carte pour obtenir un coloriage qui s’étende à la configuration. Il faut pour cela considérer l’ensemble des coloriages de chaque configuration (jusqu’à 20 000 pour une configuration), mais aussi l’ensemble des appariements par composantes bicolores (jusqu’à 1 500 000). Même pour un ordinateur moderne utilisant un algorithme efficace, cela reste un calcul non-trivial. Cette partie est évidemment hors de portée d’un humain ou d’un groupe d’humains. On ne peut que faire confiance à la machine.

Un langage commun

La formalisation de la preuve des quatre couleurs dans le système Coq signifie donc deux choses. Tout d’abord, on a prouvé formellement la correction des programmes utilisés pour vérifier la réductibilité des configurations. Mais surtout, on a pu, dans le même langage, celui de Coq, effectuer l’ensemble de la preuve, c’est-à-dire :

1. construire la théorie des graphes planaires et prouver, formellement, une série de lemmes et théorèmes,
2. écrire les programmes nécessaires pour démontrer, formellement, le lien entre ces programmes et la propriété de réductibilité,
3. vérifier la preuve des quatre couleurs, processus qui fait intervenir les propriétés (1) et l’exécution des programmes (2).

On peut donc dire que c’est la première fois qu’une preuve du théorème des quatre couleurs est entièrement écrite : les textes existants jusqu’à maintenant ressemblaient à des textes mathématiques, jusqu’à la preuve de réductibilité. Il fallait ensuite passer des mathématiques à l’informatique en changeant de langage et écrire un programme informatique ; on laissait le lecteur s’assurer qu’un résultat positif de l’exécution du programme signifiait bien l’existence d’une preuve.

Le langage de Coq évite cette rupture, puisqu’il inclut à la fois déduction et programmes. C’est parce qu’il fait appel à la programmation fonctionnelle que calcul et raisonnement peuvent s’articuler dans un formalisme comme celui de Coq.

Pour résumer la situation des preuves calculatoires, on peut donc dire d’abord que l’on a affaire à des preuves dont la vérification est hors de la portée de l’esprit humain sans assistance extérieure, et ce pour des raisons quasiment « mécaniques ». Le premier problème que cela pose est celui du langage dans lequel décrire ces preuves, puisque ce dernier doit inclure à la fois le discours mathématique traditionnel, mais aussi la possibilité de décrire des algorithmes informatiques. Les systèmes de preuve calculatoires proposent donc de tels langages hybrides, mais ils répondent aussi à la seconde interrogation à propos de l’interface entre ces deux modes : comment être sûr que le programme donné a bien les propriétés attendues, c’est-à-dire que tel ou tel résultat d’un calcul implique bien telle ou telle proposition mathématique.

D’un côté, on peut espérer que l’alliance entre raisonnement et calcul ouvre une nouvelle voie aux mathématiques : elle met à notre portée des résultats qui pour de simples raisons « mécaniques » (longueur de la preuve) étaient inaccessibles jusqu’à maintenant. On peut même imaginer l’appropriation par les mathématiciens d’un nouveau mode de recherche plus expérimental. Mais l’introduction de calculs informatiques rend plus difficile la vérification de ces résultats en même temps qu’est perdue une certaine forme d’intuition. La formalisation et la vérification informatique apparaissent comme le meilleur moyen de garantir la correction de ces nouvelles constructions mathématiques. Un atout étant que, comme évoqué plus haut, la vérification de logiciels est historiquement l’un des premiers débouchés pour la formalisation.

D’un autre côté, formaliser ces raisonnements d’un type nouveau nécessite une complexification du langage mathématique, puisqu’il faut lui incorporer un langage de programmation. Or, même si ce langage peut être plus épuré que celui qui sert à programmer un jeu vidéo, il se pose néanmoins la question du standard. On se trouve déjà dans une situation de concurrence entre plusieurs formalismes et plusieurs systèmes de preuve et la question est ouverte de savoir lesquels pourront s’établir comme des standards pour la communauté mathématique, et par quels processus. On peut toutefois penser que le défi pour les développeurs des systèmes de preuve est de les rendre suffisamment pratiques pour les faire adopter au moins par les mathématiciens dont le domaine de recherche gagnerait à être formalisé. Pour les mathématiciens, il s’agira d’apprivoiser les systèmes de preuves, techniquement mais aussi socialement, en les intégrant aux critères de publication existants.

Conjecture de Kepler ou théorème de Hales ?

La meilleure façon de ranger les oranges est celle de l’étal des marchés.
Photo : Robert Cudmore.

La question de la crédibilité des preuves mêlant raisonnement et calcul s’est reposée de manière brûlante voici peu de temps. Pendant vingt ans, la preuve du théorème des quatre couleurs est restée unique en son genre, et l’emploi important qu’elle faisait du calcul a surtout contribué à lui donner une aura particulière. Mais l’Histoire s’est répétée une première fois en 1998, lorsque Thomas Hales a proposé une preuve de la célèbre conjecture de Kepler. Là encore il s’agit d’une conjecture ancienne, puisqu’énoncée en 1611 et qui peut être expliquée dans un langage non-mathématique : il n’y a pas de façon de ranger des oranges qui soit meilleure que celle des étals des marchés.

À l’image de celle du théorème des quatre couleurs, la preuve de Hales repose sur des calculs informatiques importants. Elle est toutefois nettement plus complexe, parce que ces calculs interviennent à plusieurs niveaux dans la preuve, et surtout parce que la partie « conventionnelle », c’est-à-dire non calculatoire de la preuve, est elle aussi plus longue et utilise plus de résultats pré-existants que celle des quatre couleurs.

Thomas Hales a soumis une série d’articles décrivant sa preuve en 1999, mais ces derniers ne paraîtront qu’en 2005 ; les relecteurs ne sachant pas comment traiter les parties calculatoires. Qui plus est, ces articles seront accompagnés d’une mise en garde de l’éditeur précisant que ces parties informatiques de la preuve n’ont pas pu être vérifiées. On peut voir là le reflet d’une certaine réticence vis-à-vis de l’utilisation d’outils informatiques, mais il est indéniable que ce type de preuves est difficile à valider avec les procédures habituelles. D’une part parce que leur lecture complète nécessite des compétences en programmation. Mais aussi d’autre part parce que même pour un informaticien professionnel, la correction d’un programme est difficile à établir, pour les raisons déjà mentionnées.

Depuis cette relative mésaventure, Thomas Hales est devenu un ardent défenseur des mathématiques formelles. Qui plus est, ayant eu vent de l’effort de formalisation de la preuve des quatre couleurs, il a lancé un projet de formalisation de sa propre preuve qu’il a intitulé Flyspeck. Toutefois, il faudra sans doute attendre longtemps l’achèvement de ce projet. Cela est dû à la complexité de la preuve elle-même, mais aussi au fait que les résultats mathématiques publiés antérieurement sur lesquels elle repose ne sont pas encore formalisés.

Mise à jour : le 10 août 2014, Thomas Hales a annoncé que le projet avait abouti.

En sus de cet ambitieux projet, Hales a récemment annoncé et publié une preuve du théorème de Jordan, entièrement formalisée dans le système HOL-light.

Le monstre et la machine

Si l’ordinateur semble l’outil adapté pour dompter les monstres engendrés par les mathématiques contemporaines, ces derniers ne doivent pas tous leur caractère particulier au seul calcul. L’un des résultats les plus singuliers de l’époque récente est à cet égard la classification des groupes finis. Il s’agit là d’un résultat mathématique que l’on peut dire « conventionnel » de par son énoncé comme de sa preuve, si ce n’était leur taille : la preuve a été estimée à 15 000 pages, dispersées dans diverses publications mathématiques. Il paraît donc là aussi difficile de parler d’intuition ou d’évidence cartésienne à propos d’un tel ensemble de preuves. Une formalisation de cet important corpus serait sans doute un apport à ce délicat édifice. (À une échelle plus humaine, il faut mentionner les travaux en géométrie algébrique comme ceux de Carlos Simpson. La complexité croissante de certains de ses énoncés l’ont conduit à formaliser ses travaux en Coq).

On peut espérer voir naître de tels efforts de formalisation dans un futur très proche. Il sera particulièrement intéressant d’en observer les progrès, car ce défi recouvre deux points importants et qui restent aujourd’hui encore particulièrement délicats à maîtriser. Le premier est qu’un tel travail ne pourrait être que collectif, nécessiterait donc de coordonner un important travail d’équipe autour d’un développement. Le second concerne la question des bibliothèques rassemblant des développements pouvant être réutilisés.

Une question de style

Si la communauté mathématique témoigne d’un intérêt grandissant pour la vérification informatique du raisonnement, on doit aussi se poser la question des freins à cette évolution. Un premier obstacle à l’utilisation d’un système de preuve est la nécessité d’apprendre le langage avec lequel les preuves sont communiquées à l’ordinateur. Mais si cela demande un certain investissement initial, c’est en général un obstacle surmontable, particulièrement pour des mathématiciens rompus au langage algébrique. Un facteur plus critique actuellement reste la difficulté à construire des bibliothèques de développements mathématiques formels réellement pratiques et réutilisables. De fait, on observe qu’au début d’un développement important, les utilisateurs préfèrent encore souvent repartir de zéro plutôt que de commencer à construire sur des définitions ou des lemmes repris d’un autre travail. Ce phénomène est identifié depuis longtemps en programmation, où l’on parle souvent de la question de la « réutilisabilité du code ».

Si cette réutilisabilité ne va pas forcément de soi en mathématiques formelles, c’est que celles-ci sont particulièrement sensibles aux détails des définitions et des énoncés. Dans un texte traditionnel, on utilisera la notion de polynôme indifféremment pour désigner une classe particulière de fonctions réelles, ou une classe d’expressions algébriques (à savoir les sommes de monômes). De plus, on regardera le même polynôme parfois comme une fonction et parfois comme une expression algébrique. Si l’on travaille formellement, la fonction et l’expression sont deux objets distincts ; on peut certes définir les traductions de l’une vers l’autre, mais chaque invocation de ces traductions alourdira énoncés et preuves.

Or la lourdeur est l’écueil principal de la preuve formelle. Dans les faits, lorsqu’un développement ne peut être mené à son terme, c’est en général parce qu’à partir d’un moment il risque de crouler sous le nombre d’hypothèses locales, le nombre de petits résultats intermédiaires ou le nombre d’étapes « triviales ».

Pour éviter cela, la meilleure arme reste un choix judicieux des définitions et des énoncés, qui permettra la preuve la plus élégante possible. En d’autres termes, et c’est sans doute une bonne nouvelle, tout en étant, comme on le lui demande, un vérificateur sans âme, l’ordinateur devient également un garant du beau style mathématique.

Une première version de ce document a été publiée dans la revue Images des mathématiques en octobre 2006.