23 novembre 2012

3 commentaires — commenter cet article

Coq et caractères

Preuve formelle du théorème de Feit et Thompson

Jérôme Germoni

Une équipe du laboratoire commun Inria - Microsoft Research dirigée par Georges Gonthier a annoncé fin septembre la vérification par un ordinateur, plus précisément par l’assistant de preuve Coq, du théorème de Feit et Thompson, un résultat difficile d’algèbre prouvé en 1963 par deux cent cinquante pages ardues. La nouvelle semble susciter plutôt de la perplexité chez certains mathématiciens : qu’apporte une preuve par ordinateur à un résultat dont personne ne doute ? D’autres collègues, plus enthousiastes, saluent le tour de force de faire vérifier à un ordinateur un des fleurons de la pensée humaine.

Lacunes du discours mathématique

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

Un exemple tiré de la presse récente

La presse, pourtant exemplaire en matière de précision, est parfois amenée à corriger certaines affirmations hâtives. « En témoigne l’erratum, (la correction) qui a été publié après un article [du New York Times] du 18 octobre et repéré par Rue89. L’article concernait Ahmed Abu Khattala, suspecté dans l’attaque contre le consulat américain de Benghazi. Le premier paragraphe racontait que, alors que les autorités américaines ont promis de le traduire devant la justice, on l’avait vu récemment siroter un jus de fruit dans un hôtel de luxe. » Bruno Duvic continuait ainsi sur France Inter le 22 octobre 2012 : « Erratum ! Ah bon ? On aurait accusé cet homme à tort ? Voici le texte publié par le New York Times. “Une version précédente de cet article décrivait de façon incorrecte la boisson que Ahmed Abu Khattala buvait dans un hôtel de Benghazi, en Libye. Il s’agissait d’une boisson frappée aux fraises et non d’un jus de mangue.” » [1]

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.

« La mathématique formelle » d’après Bourbaki

Dans le premier chapitre de la Théorie des ensembles des Éléments, Bourbaki présente un texte mathématique comme un « assemblage » de « signes » choisis entre les « signes logiques » ($\Box$, $\tau$, $\wedge$ et $\neg$), les lettres (éventuellement accentuées $A$, $A'$...) et les « signes spécifiques de la théorie » (en théorie des ensembles, $\in$ ou $=$ suffisent), certains signes pouvant être surmontés de traits appelés « liens ». Certains « critères de substitution » permettent de simplifier des assemblages, des règles de construction permettent de former des assemblages, dont certains représentent des « objets », d’autres des « assertions ». Pour définir une théorie, on se donne des « axiomes » et des « schémas » permettant de transformer les termes et de déduire d’autres assemblages.

Mais « l’usage exclusif des assemblages conduirait à des difficultés typographiques et mentales insurmontables. C’est pourquoi les textes courants utilisent des symboles abréviateurs (notamment des mots de la langue ordinaire). » Il faut une cinquantaine de pages à Bourbaki pour justifier les méthodes habituelles de raisonnement et de rédaction d’un texte mathématique.

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.

PNG - 76 ko
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 16e 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].

JPEG - 153.3 ko
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.

La question des fondements et le renouveau des mathématiques constructives

La question des fondements des mathématiques a été une des préoccupations majeures au début du XXe siècle. En voici quelques acteurs majeurs : David Hilbert, Alfred North Whitehead, Bertrand Russel, Kurt Gödel... Un peu plus tard, Bourbaki a proposé sa propre formalisation. Un large consensus en ressort : les mathématiques classiques reposent désormais sur la théorie des ensembles, laquelle est décrite par les axiomes de Zermelo-Fraenkel et, souvent, l’axiome du choix.

Néanmoins, cette position n’est pas acceptée de tous : les constructivistes contestent l’existence d’un objet qu’on ne peut pas construire ; cela les conduit en particulier à rejeter une preuve par l’absurde ; ils estiment que les axiomes de la théorie des ensembles engendrent des objets « trop gros » pour notre univers. Dans ce point de vue, une preuve, c’est essentiellement un algorithme (voir ci-dessous l’exemple du PGCD). Aussi, la montée en puissance de l’informatique a sonné le renouveau du constructivisme en mathématiques.

Dans cette mouvance, on peut citer Thierry Coquand. Le nom de l’assistant de preuve Coq est une double référence à son nom et au calcul des constructions, abrégé en CoC en anglais, dont il est le fondateur et un expert.

Vladimir Voevodsky, lauréat de la médaille Fields en 2002 pour des travaux classiques (non constructivistes), travaille depuis quelques années à clarifier les fondements des mathématiques. Il organise par exemple une année spéciale à l’Institute for Advanced Study de Princeton, avec Thierry Coquand et Steve Awodey. Pour reprendre les mots d’Assia Mahboubi, le but est de « comprendre comment une meilleure description des fondements des mathématiques peut aider à déterminer le bon langage et les bonnes définitions pour des objets les plus fondamentaux (catégories, ensembles, structures), qui induiront l’intuition la plus juste, et la plus complète de ces objets, minimisant les constructions bancales, ou trop techniques, qui incitent à l’erreur. »

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.

Un exemple de preuve (non formelle) de validité d’un algorithme

Montrons que l’algorithme d’Euclide donne, étant donnés deux entiers naturels $a$ et $b$, leur PGCD, c’est-à-dire un entier naturel $d$ qui les divise tous les deux et tel que tout autre diviseur commun à $a$ et $b$ est un diviseur de $d$.

L’algorithme se termine. En effet, à chaque passage dans la boucle, la valeur de la variable $y$ diminue strictement : il y aura donc au plus $b$ passages dans la boucle.

Pour prouver que l’algorithme est correct, on met en évidence un invariant de boucle, c’est-à-dire une assertion qui est vraie au démarrage de l’algorithme et qui reste vraie après chaque passage dans la boucle : elle sera donc vraie à la fin de l’exécution.

Pour deux entiers $a$ et $b$, on note $D(a,b)$ l’ensemble de leurs diviseurs communs. L’assertion clé est :

$D(a,b)=D(x,y)$.

Montrons que c’est bien un invariant de boucle :

  • Avant le premier passage dans la boucle, on a : $x=a$ et $y=b$, si bien que l’égalité est évidente.
  • Supposons qu’au début d’un passage dans la boucle, on ait : $D(a,b)=D(x,y)$. À la fin de la boucle, on a remplacé $x$ par $y$ et $y$ par $x-qy$ (où $q$ est le quotient de $x$ par $y$). Il suffit donc de montrer que $D(x,y)=D(y,x-qy)$ : si un entier $d$ divise $x$ et $y$, il divise aussi $y$ et $x-qy$ (si $x=dx'$ et $y=dy'$, alors $x-qy=d(x'-qy')$) ; inversement, s’il divise $y$ et $x-qy$, il divise aussi $x=(x-qy)+qy$ : c’est gagné.

En sortie de boucle, la variable $y$ vaut $0$ ; notons $d$ la valeur de la variable $x$ que renvoie l’algorithme. On a, d’après ce qui précède : $D(a,b)=D(d,0)$. Or, comme tout entier divise $0$, les diviseurs communs à $d$ et $0$ sont les diviseurs de $d$, parmi lesquels $d$ est le plus grand (au sens de la divisibilité). Par suite, l’entier $d$ satisfait aux spécifications.

Mais il y a mieux ! En effet, ce qui précède montre qu’il existe un PGCD et qu’il est unique (c’est loin d’être évident a priori) ; de plus, on a un moyen de le calculer. On voit, dans cet exemple, comment un algorithme et une preuve de validité de l’algorithme prouvent un théorème (l’existence et l’unicité du PGCD).

JPEG - 25 ko
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]

L’algorithme d’Euclide et le PGCD vus par Coq

L’algorithme d’Euclide et la notion de PGCD sont des notions si basiques qu’elles font, évidemment, partie de la distribution standard du logiciel Coq. On les trouve dans cette bibliothèque d’arithmétique élémentaire, dont ce bloc dépliant est une sorte de fiche de lecture rédigée par un béotien. [8]

La page commence par la définition de la divisibilité : le critère pour pouvoir affirmer qu’un entier a divise un autre entier b, c’est de pouvoir trouver un entier q tel que b=q*a. Puis est introduite une notation infixée et viennent un grand nombre de résultats (des Lemmas), chacun suivi de preuves. Le premier de ces lemmas exprime qu’un nombre est toujours divisible par lui-même : pour le voir, il suffit de prendre q=1 dans la définition et appliquer une des règles de calcul pour simplifier 1*a en a (ring). Facile, non ?

Non, pas si facile : que veut dire la ligne qui commence par Hint ? Passons. Les deux lemmes suivants, Zmult_divide_compat_l et Zmult_divide_compat_r, expriment tous deux que si a divise b, alors ac divise bc, et ce quels que soient les entiers a, b et c ; ces lemmes coïncident à l’ordre des facteurs près (l pour « gauche », r pour « droit »). La preuve du premier est une récurrence sur c ; la preuve du second se ramène au premier en réécrivant, dans la conclusion souhaitée, a * c à la place de c * a et idem pour b ; on conclut alors trivialement...

Et ainsi de suite : on voit défiler un grand nombre de propriétés plus ou moins immédiatement identifiables et des preuves, qui utilisent les propriétés précédentes. Pour le non-spécialiste qu’est l’auteur, il est frappant de voir combien la syntaxe est presque familière. Presque, seulement...

La définition du PGCD qui suit se paraphrase ainsi : on dit qu’un entier d est un PGCD de a et b s’il est un multiple de tout entier x qui divise a et b. « On prouvera son unicité plus loin », promet un commentaire dans un cadre bleu. Viennent une série de « propriétés triviales », par exemple la dernière : la valeur absolue d’un entier a est un PGCD de a et 0.

Puis l’algorithme d’Euclide. Sans aller dans les détails, on observe deux points clés : d’une part, les lemmes Zis_gcd_for_euclid et Zis_gcd_for_euclid2 permettent de passer de a et b à b et a-q*b ou à b et b*q+r ; le lemme euclid_rec fournit l’invariant de boucle évoqué dans le bloc dépliant ci-dessus à l’assistant de preuve. La lecture de cette partie est moins facile à interpréter que ce qui précède, mais l’exécution apporte quelques éclaircissements. Essayez !

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.

Et pourtant : l’informatique est un recours inévitable...

Gilles Dowek [15] renverse cet état de fait apparemment négatif pour justifier que les mathématiciens ont besoin des ordinateurs s’ils ne veulent pas se cantonner dans des « preuves courtes ». En effet, décider si toutes les propositions démontrables en moins de dix mille pages sont vraies ou fausses est un problème décidable (il suffit d’énumérer toutes les preuves possibles, les valider ou les réfuter : c’est hors de portée d’un ordinateur en pratique, mais ça n’a aucune importance ici). Il existe donc des propositions démontrables dont la preuve la plus courte est « longue » (peut-être que le théorème des quatre couleurs est de ce type) : pour cette catégorie, l’ordinateur peut aider l’être humain en prenant en charge des portions importantes de la preuve.

Peut-être peut-on objecter que le pouvoir sémantique des mathématiques augmente et que les preuves tendent à devenir plus courtes lorsque leurs concepts deviennent plus puissants. Ou estimer qu’il n’y aura plus de source d’énergie pour faire fonctionner un ordinateur avant que la panoplie des propositions à preuve courte ne soit épuisée. À ce moment-là, l’hypothèse de Riemann sera peut-être une préoccupation subalterne.

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.

JPEG - 97.5 ko
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 ».

PNG - 13.7 ko
Icosaèdre régulier et un plan de symétrie

Définition d’un groupe

Appelons transformation d’un système ou ensemble $X$ une application bijective $g$ de $X$ dans lui-même : cela signifie qu’à tout point de $X$, on sait associer un (autre) point de $X$, et qu’il existe une « transformation inverse » $g^{-1}$, telle qu’en appliquant successivement $g$ et $g^{-1}$ (dans les deux ordres possibles), on envoie tout élément de $X$ sur lui-même.

Un groupe est alors un ensemble (non vide) de transformations d’un système satisfaisant aux conditions suivantes :

  • il contient l’inverse de chaque transformation qu’il contient ;
  • il contient la composée de deux transformations quelconques qu’il contient.

C’est la présentation classique (d’avant Sophus Lie) préférée par Vladimir Arnold à la définition abstraite. Pour ceux qui le connaissent, le théorème de Cayley garantit que cette définition est équivalente à la définition axiomatique habituelle (au moins si on travaille à isomorphisme près).

Voici un exemple : fixons un entier $n$ et soit $\alpha$ l’angle $360^\circ/n$. Les transformations consistant à tourner autour d’un point fixe d’un angle multiple de $\alpha$ forment un groupe ayant $n$ éléments, appelé groupe cyclique d’ordre $n$.

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.)

Groupes résolubles, groupes simples (version hardcore)

Un groupe $G$ est dit simple s’il n’admet pas d’autre sous-groupe distingué que le sous-groupe trivial $\{1\}$ et $G$ (un sous-groupe distingué $H$ permet de construire un groupe-quotient $G/H$). Les groupes simples jouent un peu, pour les groupes, le rôle des nombres premiers pour les entiers : des sortes de briques élémentaires.

Pour voir l’analogie, commençons par reformuler le théorème de factorisation de la façon suivante : étant donné un entier $n\ge1$, il existe une suite finie d’entiers $(n_k)_{0\le k\le r}$ telle que $n_0=1$, $n_r=n$ et, pour tout $k\ge1$, $n_{k-1}$ divise $n_k$ et $p_k=n_k/n_{k-1}$ est premier. Alors, la liste des nombres premiers $p_k$ est bien déterminée à l’ordre près. Par exemple, pour $n=6$, on a nécessairement $n_0=1$ et $n_2=6$ ; mais on peut prendre $n_1=2$, de sorte que $p_1=2$ et $p_2=3$, ou bien $n_1=3$, de sorte que $p_1=3$ et $p_2=2$.

De même, étant donné un groupe fini $G$, il existe une suite de sous-groupes $(G_k)_{0\le k\le r}$ tels que $G_0=\{1\}$, $G_r=G$, et pour tout $k\ge1$, $G_{k-1}$ est distingué dans $G_k$ et $S_k=G_k/G_{k-1}$ est simple. Alors, la suite des groupes simples $S_k$ est bien déterminée à l’ordre près.

Un groupe fini est dit résoluble si chacun des groupes simples $S_k$ est isomorphe à un groupe cyclique $\mathbb{Z}/p\mathbb{Z}$ d’ordre $p$ premier (dépendant de $k$). Cette notion est la clé mise en évidence par Galois pour décider si une équation algébrique est « résoluble par radicaux », c’est-à-dire si ses solutions peuvent s’écrire par une formule du genre $(-b\pm\sqrt{b^2-4ac})/(2a)$.

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.

Quelques vagues idées de la preuve : représentations et caractères

Partons d’une idée dont le champ d’applications est pratiquement illimité : linéariser un problème, c’est le simplifier. Par exemple, pour étudier une courbe, on l’approxime par petits morceaux par des segments de droite — on dérive. Parmi les systèmes d’équations, les systèmes linéaires sont, de très loin, les plus simples. C’est parce qu’on peut leur appliquer la puissante théorie des espaces vectoriels, l’algèbre linéaire. On y voit apparaître des groupes formés de matrices qui sont, disons, les mieux connus.

Une représentation d’un groupe est une façon de réaliser (un quotient de) ce groupe comme un groupe de matrices : en arrivant dans le monde linéaire, on a simplifié. Ici, on peut presque prendre le terme de représentation au sens commun. Si une représentation donne une image partielle, imparfaite, la connaissance de toutes les représentations permet de lire presque tout ce qu’on peut vouloir savoir sur le groupe.

Une matrice, c’est plus concret qu’un élément d’un groupe abstrait, mais c’est encore compliqué. Lorsqu’on dispose d’une représentation où les coefficients des matrices sont des nombres complexes, on peut construire son caractère : à chaque élément du groupe, on associe un nombre, la trace de sa matrice dans la représentation. Le terme vient du fait stupéfiant suivant : le caractère caractérise la représentation, c’est-à-dire que pour connaître une représentation (à isomorphisme près), il suffit de connaître son caractère. En remplaçant la matrice par sa trace, on pouvait craindre de perdre de l’information : il n’en est rien.

On a déjà signalé que le théorème de Feit-Thompson avait été imaginé par Burnside. Ce dernier a démontré un théorème beaucoup plus facile, mais de même nature :

Tout groupe fini dont le nombre d’éléments n’a que deux facteurs premiers est résoluble.

Ce résultat est une illustration typique de la théorie des représentations : une heure devrait suffire pour en convaincre un étudiant de M1 en partant de « rien ». La preuve repose sur des propriétés arithmétiques des caractères des représentations du groupe (propriétés d’intégralité).

Pour le théorème de Feit-Thompson, les représentations complexes ne suffisent pas : il faut aussi étudier les représentations sur les corps dont la caractéristique divise l’ordre du groupe, et c’est beaucoup, beaucoup plus compliqué (voici l’obstacle le plus évident : une matrice qui annule un polynôme scindé à racines simples, tel que $x^p-1$, est diagonalisable sur les complexes, mais en général, pas sur un corps de caractéristique $p$).

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à. »

Classification des groupes finis simples (10 à 20000 pages dans un bloc dépliant...)

Le théorème de classification des groupes finis simples, annoncé en 1983, exprime grossièrement qu’un groupe fini simple est isomorphe à l’un des suivants :

  • un groupe cyclique d’ordre premier $\mathbb{Z}/p\mathbb{Z}$,
  • un groupe alterné sur $5$ lettres ou plus,
  • un groupe fini de type de Lie, i.e. un groupe de matrices analogue à celui des matrices inversibles sur un corps fini,
  • un des vingt-six « groupes sporadiques », symétries d’objets exceptionnels qui n’entrent dans aucune des séries précédentes.

Le plus gros des groupes sporadiques est le monstre évoqué ci-dessus : il contient environ $8\cdot10^{53}$ éléments.

Dans cette perspective, on peut reformuler le théorème de Feit et Thompson ainsi : tout groupe simple de cardinal impair est un groupe cyclique d’ordre premier.

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 :

Plus difficile, en anglais :

P.S. :

L’auteur tient à remercier Cédric Bonnafé, Damien Gayet, la personne qui se cache sous le pseudo de goulu, Assia Mahboubi, Jean-Michel Muller, Olivier Reboux, Luc Ségoufin et Romuald Thion pour leurs relectures attentives, les corrections et toutes les explications qu’ils ont apportées et les précisions qu’ils ont demandées, dont l’article a substantiellement bénéficié.

Notes

[1An earlier version of this article misidentified the beverage that Ahmed Abu Khattala was drinking at the hotel. It was a strawberry frappe, not mango juice, which is what he had ordered..

[2Cédric Villani a présenté une conférence sur la meilleure et la pire des erreurs de Poincaré à Paris, Lille, Montpellier, Nancy, Lyon... à l’occasion du centenaire de la mort de Poincaré.

[3Cet article est paru dans la prestigieuse revue Inventiones Mathematicae. Le « théorème » dont Neeman donne un contre-exemple semblait très naturel aux experts de géométrie algébrique, si bien qu’il avait été largement utilisé pendant quarante ans et que sa réfutation a causé bien des mécontentements.

[4Assia Mahboubi, membre de l’équipe de Georges Gonthier, nous explique que la première utilisation de l’ordinateur est vraiment très proche du théorème des quatre couleurs : on travaille jusqu’à réduire la conjecture à l’examen d’un nombre fini, mais très grand, de configurations qui pourraient être un contre-exemple. Pour la seconde, il s’agit d’établir un grand nombre d’inégalités portant sur certaines fonctions de plusieurs variables : il est très difficile de s’affranchir de toutes les source d’erreurs possibles dans les logiciels ou programmes qui permettent d’établir ce genre d’ inégalités en un temps raisonnable.

[5Nicolas Bourbaki conclut l’introduction de sa Description de la mathématique formelle, loc. cit., ainsi : « En résumé, nous croyons que la mathématique est destinée à survivre, et qu’on ne verra jamais les parties essentielles de ce majestueux édifice s’écrouler du fait d’une contradiction soudain manifestée ; mais nous ne prétendons pas que cette opinion repose sur autre chose que sur l’expérience. C’est peu, diront certains. Mais voilà vingt-cinq siècles que les mathématiciens ont l’habitude de corriger leurs erreurs et d’en voir leur science enrichie, non appauvrie ; cela leur donne le droit d’envisager l’avenir avec sérénité. »

[6Preuve formelle, le théorème des quatre couleurs. Notices of the American Mathematical Society 55, n°11, 2008.

[7Puisque la certification est dévolue à l’ordinateur, on peut se demander comment il pourrait trouver un invariant de boucle comme l’assertion $D(a,b)=D(x,y)$ de l’algorithme d’Euclide. La réponse, c’est que c’est l’humain qui doit l’indiquer... et l’ordinateur se contente de vérifier que l’assertion est bien satisfaite en entrée de boucle et reste vraie à chaque passsage.

[8La bibliothèque est en anglais ; la partie qui concerne le PGCD commence plus précisément ici ; la description n’est pas celle de la dernière version de Coq, que l’on trouve ici, mais elle est plus détaillée que cette dernière ; enfin, il est instructif de copier-coller les instructions pour voir ce que Coq en fait, cela suffit pour justifier l’installation du logiciel...

[9Par exemple : théorème de réciprocité quadratique (Russinoff, 1990), théorème des quatre couleurs (Gonthier et Werner, 2004), jusqu’au théorème des nombres premiers (Harrison, 2008).

[10Par exemple, réglage des atterrissages dans un aéroport ou circulation des paquets de données sur Internet...

[11Par exemple, vérifier que tout nombre pair inférieur à $10^{12}$ est somme de deux nombres premiers donne une certaine confiance dans la conjecture de Goldbach mais en soi, cela ne fait pas approcher de sa preuve.

[12Le logiciel n’était pas certifié : il n’a fallu que quelques jours après l’accident pour comprendre, grâce à des méthodes automatiques de détection de bugs, l’origine du problème. En revanche, le logiciel avait été utilisé sans problème avec son bug sur les fusées Ariane 4 : l’erreur ne pouvait pas se produire car les données numériques étaient différentes. Cela illustre la différence entre la confiance que donnent les tests, même s’ils se déroulent pendant des années, et celle qu’apporte la certification. Pour les applications critiques, la preuve formelle est irremplaçable.

[13L’expression est le titre d’un article de Benoît Rittaud (dans sa version imprimée des Dossiers de La Recherche, n° 46, décembre 2011) sur la recherche d’une preuve formelle de la conjecture de Kepler.

[14Gilles Dowek : L’inévitable recours à l’informatique. Les dossiers de La Recherche, n° 46. Décembre 2011. Contre l’espoir de Hilbert, on pourrait mentionner également le théorème d’incomplétude de Gödel, dès 1931, qui a été un coup de tonnerre : il existe des assertions vraies qui ne sont ni démontrables, ni réfutables.

[15Gilles Dowek, loc. cit.

[16Formal Proof. Notices of the AMS, loc. cit. (Voilà qui n’est pas terrible, poursuit-il, mais qui améliore le bug et demi par ligne qu’un programmeur introduirait en moyenne dans sa première version.)

[17Naturellement : in fine, une preuve, un ordinateur, un langage... sont des artefacts humains, donc faillibles.

[18Yves André : Idées galoisiennes, article publié à l’occasion du bicentenaire d’Évariste Galois.

[19Il y a une famille d’exceptions : les groupes cycliques d’ordre premier sont simples et commutatifs. Pour étayer un peu l’assertion, on peut remarquer que dans un groupe abélien, tout sous-groupe est distingué ; un groupe résoluble contient « beaucoup » de sous-groupes distingués ; à l’opposé, un groupe simple n’en contient essentiellement aucun.

[20En combinatoire, compter les objets, c’est étudier leur géométrie (discrète).

[21Voir son article sur le théorème des quatre couleurs référencé dans le PS.

Crédits images

Image à la une — Le logo a été composé sous les directives inspirées d’Amaury Thuillier.
Conjecture de Kepler décrit l’empilement de sphères le plus dense possible : démontrée ou pas ? — Wikipedia anglaise — Licence Creative Commons
Théorème des quatre couleurs — Wikimedia Commons — Domaine public
Coq au secours d’Euclide — Wikimedia Commons — Licence Creative Commons
Conjecture de Kepler et théorème des quatre couleurs : démontrés ou pas ? — Wikimedia Commons — Licence Creative Commons et domaine public
John Griggs Thompson et Walter Feit — Oberwolfach — Licence Creative Commons
Icosaèdre régulier et un plan de symétrie — Image réalisée avec Sage

Affiliation de l'auteur

Jérôme Germoni : Institut Camille Jordan, Université Lyon 1

Commentaires sur l'article

Pour citer cet article : Jérôme Germoni, « Coq et caractères »Images des Mathématiques, CNRS, 2012.

En ligne, URL : http://images.math.cnrs.fr/Coq-et-caracteres.html

Si vous avez aimé cet article, voici quelques suggestions automatiques qui pourraient vous intéresser :