Lacunes du discours mathématique

Malgré tous les efforts de son auteur, un texte risque d’être entaché d’inexactitudes.

L’Éden mathématique serait, par contraste, le lieu des vérités éternelles et inattaquables où de telles imprécisions n’auraient pas cours. Une preuve mathématique devrait partir d’axiomes si naturels et procéder par étapes si élémentaires qu’elle doit devenir évidente pour tout autre mathématicien, ce qui assure un caractère irréfutable au théorème. Beau programme, qui trouve son origine dans les Éléments d’Euclide, et précisé vingt-cinq siècles plus tard, dans les Principa Mathematica d’Alfred Whitehead et Bertrand Russell ou les Éléments de mathématique de Nicolas Bourbaki.

Mais si on devait détailler la rédaction à ce point, la démonstration du moindre fait significatif deviendrait longue au point d’en être impossible à lire, voire à écrire. Aussi, les textes mathématiques regorgent de raccourcis qui, implicitement, signifient : « il est évident que... » Une preuve est donc écrite pour un public particulier d’élèves, d’étudiants, de chercheurs... avec un niveau de détail adapté à ce public (ou, du moins, qui devrait l’être) : remplacer $1+2+\cdots+n$ par $n(n+1)/2$ est un problème difficile pour un élève de troisième, c’est une évidence pour un mathématicien professionnel. Il reste donc au lecteur des étapes à combler. La formalisation que Bourbaki affirme possible en principe ne semble pas réalisable par un être humain ; de plus, elle obscurcirait plutôt les choses et on n’aurait rien à y gagner.

Un théorème des Principia Mathematica de Whitehead et Russell et une preuve sans mots : thèse et antithèse

En général, combler les étapes manquantes du discours mathématique se fait sans mal. Sinon, modulo les convenances sociales, le lecteur (élève, mathématicien, relecteur d’une revue...) est en droit de demander des éclaircissements à l’auteur (professeur, chercheur...). Mais il peut arriver qu’une preuve soit longue et ardue et que sa validation le soit aussi : celle de la conjecture de Poincaré par Grigori Perelman a pris environ quatre ans aux experts du sujet.

Erreurs et mathématiques

Par ailleurs, dans les implicites d’une preuve, peuvent se glisser des erreurs. Les articles spécialisés et les livres en sont parsemés : ce sont souvent des fautes mineures, comparables à la confusion entre fraise et mangue, que le lecteur repère et corrige tout de suite. Il peut même ne pas les voir, si sa démarche mentale est assez active pour qu’il suive les grandes lignes de la preuve et en reconstitue les détails lui-même. Mais cela peut être plus sérieux : après l’annonce en 1993 par Andrew Wiles de la démonstration de la dernière étape du dernier théorème de Fermat, les experts ont découvert un argument faux, que Wiles a réussi à corriger avec Richard Taylor en quelques mois.

Les erreurs sont un élément de la vie mathématique. Certaines restent célèbres, telle l’erreur féconde commise par Poincaré pour le prix du roi Oscar [2]. Mais on en trouve de nombreuses autres dans l’histoire mouvementée du 16^e problème de Hilbert. Certaines erreurs en mathématiques sont corrigées, d’autres encore ne sont jamais détectées. On en comprend bien l’origine : avant d’avoir été poli par la pensée comme un galet par le ressac, un concept reste fuyant et malcommode, et ce qui paraît « évident » dans la fulgurance de l’intuition peut se révéler faux plus tard.

En tout état de cause, la validité d’une preuve est un acquis social : c’est une communauté qui donne le quitus. En pratique, la plupart des théorèmes ne font aucun doute : ils ont été compris et démontrés tant de fois... Mais cette validation peut être remise en cause. Certaines preuves d’Euclide ont été jugées valables pendant des millénaires, mais des géomètres de la trempe de David Hilbert les ont reprises et complétées. Plus grave, la preuve par Kempe en 1879 du théorème des quatre couleurs a été jugée correcte pendant une dizaine d’années avant qu’une faille majeure n’y soit détectée. Pour un exemple plus récent, le titre d’un article d’Amnon Neeman paru en 2002 est explicite : “A counterexample to a 1961 ’theorem’ in homological algebra” [3].

Conjecture de Kepler et théorème des quatre couleurs : démontrés ou pas ?

Dans un registre différent, la communauté mathématique s’est déclarée incapable de valider complètement la démonstration de la conjecture de Kepler soumise par Thomas Hales vers 1999 à l’un des journaux les plus prestigieux, Annals of Mathematics. L’article a bien été publié mais avec des réserves : la preuve repose de façon cruciale sur des calculs sur ordinateur à deux reprises [4] Aucune erreur n’est connue dans la preuve mais même son auteur exprime des réserves à son sujet, au point qu’il a lancé un programme sur une vingtaine d’années pour fabriquer une preuve formelle.

En bref, presque tous les mathématiciens sont très confiants dans la robustesse de l’édifice mathématique [5] mais ils savent que des erreurs peuvent s’y glisser.

Une preuve inattaquable : la preuve formelle ?

On peut chercher à améliorer la situation grâce aux assistants de preuve. Commençons par une idée banale pour un informaticien : on peut prouver mathématiquement la validité de certains algorithmes.

Coq au secours d’Euclide

Un assistant de preuve est un logiciel spécialement dédié à la validation de preuves de théorèmes. On met ainsi en œuvre le programme lancé par Euclide : réduire chaque étape de la preuve à une évidence élémentaire, que même un ordinateur peut vérifier automatiquement (sans recours à l’intuition du lecteur ou à sa culture mathématique, en particulier). Comme le décrit Georges Gonthier, « l’idée est d’écrire un code qui décrit non seulement ce que la machine doit faire, mais aussi pourquoi elle doit le faire — une preuve formelle de correction. La validité de la preuve est un fait mathématique objectif qui peut être vérifiée par un programme différent. » [6] L’informaticien traduit la preuve dans un langage que peut intégrer l’assistant de preuve, ici le langage Coq, ce qui donne une preuve très longue ; s’y ajoute un certificat de correction de la preuve, produit par l’assistant de preuve, qui écarte la possibilité d’erreurs de calcul ou de raisonnement. On obtient ainsi une preuve formelle. La preuve se trouve ainsi beaucoup plus détaillée que quand elle était écrite par un humain et l’assistant de preuve procède à un examen beaucoup plus approfondi qu’une équipe humaine.

De l’algorithme d’Euclide à la description d’une preuve formelle

En extrapolant l’exemple de l’algorithme d’Euclide, on peut imaginer ce qu’est une preuve formelle :

• le rôle de l’algorithme est joué par formalisation de la preuve elle-même : écrite initialement par un humain (dans l’exemple du jour, Feit et Thompson en 1963), elle est traduite par un humain (Georges Gonthier et son équipe) en langage compréhensible par l’ordinateur (le langage de Coq) ;
• l’assistant de preuve (Coq) vérifie et certifie la validité du code ainsi écrit. [7]

La formalisation complète d’une preuve est, on l’a dit, un travail quasiment insurmontable pour un être humain : c’est ce qui explique que le processus prenne six ans pour une équipe entière pour un théorème de la difficulté de celui de Feit-Thompson. Mais, par les progrès de l’informatique et du matériel, sa vérification intégrale est devenue accessible à un ordinateur, ce qui donne une motivation pour un travail titanesque. La preuve formelle est un champ de recherche qui se développe en informatique depuis plus de quarante ans. Les experts font généralement remonter le domaine au système Automath élaboré en 1967 par le visionnaire Nicolaas de Bruijn, disparu cette année à 93 ans. Mais depuis, de nombreux théorèmes classiques ont reçu une preuve formelle [9].

La formalisation et la certification de preuves mathématiques s’inscrit dans une branche plus large de l’informatique, la certification de systèmes divers : processeurs, logiciels, matériels, protocoles [10]. Longtemps, la seule façon de s’assurer que quelque chose allait fonctionner conformément aux spécifications, c’était de la tester. L’analogue mathématique serait la vérification d’un énoncé sur un grand nombre d’exemples [11]. La certification par un système indépendant apporte un degré de confiance supplémentaire, de nature différente : l’analogue mathématique, c’est une preuve de l’énoncé. La certification est particulièrement cherchée pour les systèmes dits critiques, dont le dysfonctionnement aurait des conséquences plus graves que la confusion entre deux boissons sucrées : l’explosion de la première fusée Ariane 5 est due à une erreur « mineure » d’un logiciel [12] ; comme passager, on souhaite que les calculateurs d’un avion présentent les meilleures garanties de confiance, etc. Un autre exemple célèbre où la certification a été utile, mais un peu tardive, est le bug de la division du Pentium, qui a conduit Intel à rappeler à grands frais une génération de processeurs en 1994 et à investir dans la certification : depuis lors, Intel fait prouver formellement ses algorithmes arithmétiques (travaux de John Harrison entre autres). L’avantage du domaine mathématique pour ces questions, c’est que l’on n’a pas à affronter l’imperfection du réel.

Vérifier la preuve, pas trouver la preuve

Attention : il faut distinguer la démarche de certification de preuve que l’on vient de décrire de la recherche d’une preuve qu’effectuerait l’ordinateur plus ou moins seul. Ici, les ambitions sont moindres : on cherche à valider une preuve existante, à donner « la preuve de la preuve » [13].

Bien sûr, il serait beaucoup plus ambitieux d’espérer programmer l’ordinateur pour qu’il démontre lui-même le théorème à partir de son énoncé. David Hilbert rêvait, dès 1928, d’un algorithme universel pour décider de la véracité d’une assertion mathématique. Mais en 1936, Alonzo Church et Alan Turing ont démontré indépendamment « qu’un tel algorithme ne pouvait exister. Avant même la construction des ordinateurs, le théorème d’indécidabilité de la démontrabilité fixait donc l’existence d’une limite intrinsèque à leur utilité en mathématiques. » [14] En revanche, valider ou infirmer la preuve d’une assertion mathématique est un problème décidable, c’est-à-dire qu’un ordinateur peut le résoudre (en principe).

Pour reprendre une image que l’on trouve déjà chez Bourbaki (loc. cit.), quiconque connaît les règles des échecs peut vérifier si une partie les respecte ; mais ça ne suffit pas, loin de là, pour être un bon joueur. Un ordinateur programmé pour démontrer des théorèmes, qui ferait des déductions dans un ordre méthodique (par ordre lexicographique des preuves possibles ?) ou au hasard, aurait bien peu de chances de démontrer le théorème des quatre couleurs ! Encore moins qu’un logiciel qui essaierait de retrouver les quelque 260000 caractères de Cyrano de Bergerac en commençant par « aaaa... » ou en les choisissant au hasard.

Validation de la validation de la preuve...

Bien. Mais qui valide l’ordinateur qui certifie la preuve ? Qu’est-ce qui prouve que l’ordinateur fait mieux qu’attendre un moment (pour la crédibilité) et tirer au sort pour répondre « oui, la preuve est correcte » ou « non » ? D’après Thomas Hales, il y aurait dans tout programme un bug toutes les 500 lignes de code. [16]

Ce qui fonde la confiance dans une preuve formelle, c’est que l’ensemble de l’assistant de preuve est contrôlé par une toute petite partie, qu’on appellera le noyau du logiciel. La taille du noyau est suffisamment petite (500 lignes environ) pour pouvoir être scrutée par un humain ; de plus, il a été (at)testé sur un grand nombre de situations variées. Même s’il n’est pas capable de se certifier lui-même (théorème d’incomplétude de Gödel oblige), le noyau est capable de certifier le reste de l’assistant de preuve.

Il y a un deuxième étage de validation du système : en effet, un assistant de preuve est écrit dans un langage « de haut niveau », c’est-à-dire très éloigné de l’assembleur qu’utilise le processeur. Il faut donc le compiler, et il est connu qu’il n’existe pas de compilateur parfait. Néanmoins, Xavier Leroy travaille avec d’autres et avec succès à la certification de compilateurs, ce qui permet d’espérer pour bientôt de garantir cet aspect.

Résumé des épisodes précédents

Une preuve formelle est une formalisation d’une preuve, c’est-à-dire une traduction purement symbolique en langage informatique d’une preuve écrite par un être humain, et un certificat de validité de cette preuve fournie par un logiciel spécialisé appelé assistant de preuve, qui vérifie que toutes les étapes de la démonstration sont correctes et qu’elle démontre bien ce qu’elle affirme démontrer. La confiance dans l’assistant de preuve vient d’un examen et de tests approfondis du noyau et de la validation du reste par ledit noyau. Tout cela donne une confiance nouvelle dans la preuve.

Au bilan, une preuve formelle diminue énormément la possibilité d’erreurs mais elle ne permet pas d’atteindre une certitude philosophique. [17]

Après ces longues généralités sur la preuve formelle, venons-en au théorème qui fait l’objet de l’annonce.

John Griggs Thompson et Walter Feit

Théorème de Feit-Thompson

Énoncé comme une conjecture par William Burnside en 1911, le théorème de Feit-Thompson s’exprime en très peu de mots.

Tout groupe fini dont le nombre d’éléments est impair est résoluble.

De façon équivalente : tout groupe simple ayant un nombre impair d’éléments est cyclique. La théorie des groupes est la formalisation mathématique de l’idée de symétries. Alexandre Grothendieck « n’hésite pas à parler de l’invention du zéro et de l’idée de groupe comme deux des plus grandes inventions mathématiques de tous les temps » [18]. Le concept de groupe traduit l’idée de symétrie, de transformation. Un groupe fini est donc constitué d’un nombre fini de « transformations ».

Icosaèdre régulier et un plan de symétrie

Parmi les groupes, les plus simples sont les groupes dits commutatifs. Cela signifie que l’ordre des transformations n’importe pas : si je me déplace de 3 mètres vers le sud puis de 5 mètres vers l’est, je me retrouve au même endroit que si je fais les déplacements dans l’ordre inverse. Mais la plupart des groupes ne sont pas commutatifs. Si, d’une position donnée, j’avance droit devant moi sur 5 mètres avant de tourner d’un quart de tour, je ne me retrouve pas au même endroit que si je commence par tourner, puis que j’avance. Cela illustre le fait que le groupe des déplacements du plan n’est pas commutatif.

Voici une idée simple (et discutable) : un groupe commutatif, c’est facile à étudier. Les groupes résolubles sont, en un certain sens, « presque commutatifs ». Les groupes simples sont, eux, aussi éloignés que possible de la commutativité [19]. Ainsi, les groupes simples sont compliqués... Ce sont plutôt eux qui intéressent les experts, même lorsqu’ils étudient le théorème de Feit-Thompson. On en connaît des familles infinies et, en essayant de prouver que la liste était complète, on a été amené à en construire un certain nombre d’autres.

Le plus gros d’entre eux, imaginé par Bernd Fischer et Robert Griess en 1973 et défini par Griess en 1982, répond au doux nom de « monstre ». Lorsqu’on avait juste découvert le monstre, Jean-Pierre Serre, pour impressionner son collègue astrophysicien au collège de France, lui aurait dit : « Vous savez, ce nouveau groupe a plus d’éléments qu’il n’y a d’électrons dans le Soleil. Mais là où nous allons vous impressionner, c’est que nous savons que ce nombre est pair ! » C’est précisément le théorème de Feit-Thompson qui permet de l’affirmer. (En fait, « ce nombre » est parfaitement connu, voir par exemple le lien ci-dessus.)

Une bonne part de la beauté du théorème de Feit-Thompson vient du contraste entre la concision de son énoncé et la difficulté de sa preuve ; son hypothèse est de nature « géométrique » [20], la conclusion est de nature algébrique, et la preuve utilise une théorie qui n’apparaît ni dans l’hypothèse, ni dans la conclusion, que ce théorème a bien contribué à développer : la théorie des représentations.

On voit là un intérêt majeur de la preuve humaine : faire émerger des concepts féconds, qui peuvent s’appliquer à d’autres contextes et être sources de nouvelles questions. Une preuve formelle irréprochable n’a pas cette vertu cardinale — mais son élaboration peut l’avoir, d’après Georges Gonthier [21].

Un tour de force

L’annonce récente de la vérification de la preuve du théorème de Feit-Thompson comporte quelques chiffres : six ans de travail presque à temps plein pour une équipe entière, 170000 lignes de code, 15000 définitions, 4200 théorèmes... On peut presque penser que c’était plus d’effort de faire démontrer par ordinateur un résultat déjà connu que d’en produire la première preuve humaine en 1963.

C’est qu’avant d’entrer dans la preuve proprement dite, il a fallu implanter dans le système Coq l’univers mathématique dans lequel se déroule la preuve : les groupes finis et leurs propriétés de base, la théorie des représentations. Assia Mahboubi, membre du projet, confie : « Au début, il n’y avait pratiquement que les nombres naturels, les booléens et les listes. Tout le reste (ensemble finis, polynômes, nombres rationnels, algébriques, structures diverses, etc.) a été fait pendant les six ans. » Ce travail préliminaire semble occuper plus des deux tiers du code et près de 95% des définitions. Une fois fait, il a fallu certifier pas à pas la preuve du théorème, telle qu’elle est écrite dans les livres récents Local Analysis for the Odd Order Theorem par H. Bender and G. Glauberman (Cambridge University Press) et Character Theory for The Odd Order Theorem par T. Peterfalvi (Cambridge University Press).

Perspectives

Après la preuve formelle du théorème des quatre couleurs par le même Georges Gonthier et Benjamin Werner en 2004, le théorème de Feit-Thompson est le deuxième résultat mathématique marquant dont la preuve est certifiée par ordinateur. Leurs statuts sont différents. Pour le problème des quatre couleurs, la preuve de 1976 inspirait une certaine méfiance, que ce soit pour la partie humainement lisible que pour les calculs sur machine ; en revanche, personne n’utilise trop le résultat, qui est une fin en soi. Au contraire, pour le théorème de Feit-Thompson, la preuve de 1963 ne repose sur aucun calcul sur ordinateur et elle a prouvé sa solidité par l’examen de dizaines d’experts et c’est le point de départ de la gigantesque classification des groupes finis simples. Aussi, comme le dit Assia Mahboubi, « le succès de ce projet fournit des bibliothèques de mathématiques vérifiées très variées du fait de la variété des domaines qui doivent être combinés pour mener à bien la preuve du théorème de Feit-Thompson. Ce qui fournit une infrastructure pour essayer de construire d’autres théories formelles et d’autres preuves au-dessus de celle-là. »

C’est peut-être dans cette direction que la preuve formelle du théorème de Feit-Thompson est la plus prometteuse. En effet, cette classification est « énorme » : quelque 20000 pages réparties dans 500 articles de plus de 100 auteurs. Si énorme qu’aucun spécialiste ne peut affirmer la comprendre entièrement. Aussi, elle suscite quelques doutes : démontrée, pas démontrée ? Ces doutes sont d’autant plus légitimes qu’une partie de la preuve reposait sur un manuscrit non publié de quelque 800 pages (!) de Geoffrey Mason ; cette partie a été publiée en 2004 sous forme de deux livres de 500 et 800 pages (!!) de Michael Aschbacher et Stephen D. Smith. Les efforts ne se sont pas arrêtés après l’annonce du résultat ; de nouveaux travaux ont permis de simplifier des pans entiers de la démonstration. Malgré cela, elle reste surhumaine.

On peut imaginer qu’une preuve formelle donnerait plus de confiance dans la classification. Pour l’instant, c’est un horizon : s’il a fallu 6 ans pour vérifier 250 pages d’une preuve bien nettoyée, la vérification de la classification sera titanesque. Mais les progrès pourraient être rapides !

Références

Voici quelques lectures accessibles :

• Annonce officielle de la vérification complète sur le site d’Inria et description du projet (en anglais) : Theorem Proof Gains Acclaim sur le site de Microsoft Research ;
• Cédric Villani : Un classique revisité, Le Monde (3 novembre 2012 — accès réservé aux abonnés).
• Jean-Paul Delahaye : Du rêve à la réalité des preuves sur Interstices (juin 2012, antérieur à la fin du projet Feit-Thompson) ;
• Assistant de preuve sur Wikipedia.fr ;
• Les dossiers de la Recherche n°46 (décembre 2011), en particulier :
  • « L’informatique renouvelle les mathématiques » : entretien avec Gérard Berry,
  • Gilles Dowek : « L’inévitable recours à l’informatique »,
  • Benoît Rittaud : « Apporter la preuve de la preuve » ;
• Autres articles sur le site de La Recherche :
  • Gilles Dowek, interrogé par Benoît Rittaud : « Une preuve formelle du théorème des 4 couleurs » vers 2004 ;
  • Benoît Rittaud : La conjecture de Kepler démontrée à 99 %
• Pour une tout autre approche de la vérification de preuves, fondée sur des critères probabilistes, on pourra s’intéresser aux travaux d’Irit Dinur.
• Pour une discussion des mots « vrai », « démontrable », « probable », « presque sûr », « calculable », « cohérent », « effectif », « décidable »... on pourra lire cet article et les commentaires qui l’accompagnent.

Plus difficile, en anglais :

• Dossier spécial sur la preuve formelle dans les Notices of the American Mathematical Society, vol. 55, number 11 (2006) (plus difficile et en anglais ; les articles sont peut-être réservés aux abonnés) :
  • Thomas Hales : Formal Proof
  • Georges Gonthier : Formal Proof—The Four-Color Theorem
  • John Harrison : Formal Proof—Theory and Practice
  • Freek Wiedijk : Formal Proof—Getting Started