Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Echos de la recherche Coq et caractères Preuve formelle du théorème de Feit et

Echos de la recherche 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 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 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 par 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 1 + 2 + ⋯+ n n(n + 1)/2 Coq et caractères - Images des mathématiques http://images.math.cnrs.fr/Coq-et-caracteres.html 1 of 9 21/06/2013 14:09 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]. 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 Coq et caractères - Images des mathématiques http://images.math.cnrs.fr/Coq-et-caracteres.html 2 of 9 21/06/2013 14:09 Coq au secours d’Euclide La question des fondements et le renouveau des mathématiques constructives 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 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 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 uploads/s3/ coq-et-caracteres-images-des-mathematiques-lemonde.pdf