Une preuve sur les nombres premiers
À l’école, tout un chacun apprend à faire des calculs corrects, en appliquant les méthodes qu’on lui enseigne. Ces mécanismes ou algorithmes permettent à l’élève de fournir un résultat toujours juste, pourvu qu’il les applique exactement. La validation de tels algorithmes se fonde sur des théorèmes et propriétés plus ou moins compliqués. Comment montrer que cela marche toujours, et qu’un petit cas particulier n’a pas été omis ? Il faut présenter une preuve complète jusqu’au moindre détail. Un travail qui peut se révéler titanesque. L’informaticien propose d’automatiser ce processus. La machine, c’est bien connu, ne fait pas d’erreur… humaine. Même si elle est susceptible de faire des erreurs de calcul, mais ceci est une autre histoire. Une preuve automatique est donc plus sûre, mais pas forcément plus simple, qu’une démonstration faite à la main. Exemple sur un algorithme relatif aux nombres premiers, qu’une équipe de l’INRIA a validé sur ordinateur.
De la démonstration mathématique…
Le système Coq a été utilisé pour valider cet algorithme.
À partir de la fin des années 1960, l’Américain Donald Knuth a publié un ouvrage qui allait devenir une véritable bible pour les informaticiens : « The Art of Computer Programming » (« L’art de la programmation informatique »), qui recense de nombreux algorithmes. Dans le premier tome, il propose un algorithme qui calcule les n premiers nombres premiers, pour un entier n quelconque.
Pour valider cet algorithme, les chercheurs ont choisi d’utiliser l’un des systèmes de preuves formelles existants, le système Coq développé à l’INRIA. L’algorithme est très simple, et tient en quelques lignes. L’aventure de sa preuve automatique n’a pourtant pas été dénuée d’obstacles, comme l’explique Laurent Théry, chercheur à l’INRIA Sophia-Antipolis.
L’algorithme de Knuth contient en effet une optimisation d’apparence anodine. Or celle-ci repose sur une propriété profonde des nombres premiers, appelée conjecture de Bertrand. La preuve de l’algorithme de Knuth devait donc inclure la preuve de cette conjecture. La première démonstration en a été fournie par Pafnuty Lvovich Tchebychev entre 1850 et 1854. Mais cette démonstration est longue et compliquée. Laurent Théry s’est tourné vers celle du grand mathématicien Paul Erdös. Plus récente, elle est surtout bien plus simple. Erdös l’a explicitée pour le cas général, laissant au lecteur le soin d’étudier les cas particuliers, comme cela est fréquent en mathématiques.
Pour produire la liste des n premiers nombres premiers, l’algorithme proposé par Donald E. Knuth procède de proche en proche. Le calcul du nombre premier de rang n (le nième nombre premier) s’appuie en effet sur le calcul des n-1 nombres premiers précédents.
Principe de base
Supposons que l’on ait déjà trouvé les quatre premiers nombres premiers. La liste d’entrée est donc : 2, 3, 5, 7. Pour trouver le nombre premier suivant, on considère les nombres supérieurs au dernier trouvé, soit 7 dans cet exemple.
Première remarque : il est d’emblée possible d’exclure les nombres pairs. Les nombres pairs sont en effet divisibles par 2, donc non premiers. On exclut donc 7+1, 7+3, 7+5, etc. Restent à tester : 7+2, 7+4, 7+6, etc.
Deuxième remarque : comment savoir par exemple si 7+2 = 9 est premier ou pas ? Il suffit de vérifier qu’il n’est divisible par aucun des nombres premiers qui lui sont inférieurs (soit 2, 3, 5 ou 7). De toute évidence 9 n’est pas premier, puisqu’il est divisible par 3.
Quel est le premier nombre premier après 7 ? Après avoir réitéré la démarche, on trouve 11.
Un peu d’astuce
Si un nombre entier k est composite (non premier), il peut s’écrire comme le produit de deux nombres entiers p et q : k = pq
Or ces deux nombres p et q ne peuvent être simultanément supérieurs à la racine carrée s de k, car alors leur produit serait supérieur à k. En effet, si p > s et q > s, alors p x q > s x s, soit p x q > k.
D’où le petit théorème : si k est non premier, il possède forcément un diviseur plus petit ou égal à sa racine carrée. Inversement, s’il ne possède pas de diviseur plus petit ou égal à sa racine carrée, c’est qu’il est premier.
Exemple : pour déterminer si 11 est premier, il suffit de tester sa divisibilité par 2 et par 3, car la racine carrée de 11 est 3,3166…
Le théorème de Bertrand
Celui-ci énonce qu’il existe toujours au moins un nombre premier entre k et 2k. Autrement dit, le premier nombre premier supérieur à k, appelons-le j, est forcément inférieur à 2k.
Conséquence
Pour trouver j, on utilise à la fois le théorème de Bertrand et le petit théorème précédent. On teste tous les nombres impairs « i » compris entre k+2 et 2k. Pour chaque « i », il suffit de regarder s’il est divisible par tous les nombres premiers inférieurs ou égaux à la racine carrée de « i ».
Pour vérifier si un nombre i compris entre k et 2k est premier, il suffit de parcourir la liste des nombres premiers déjà calculés, en partant du plus petit, c’est-à-dire 2, comme suit :
Si le nombre premier p considéré divise i, on peut s’arrêter là.
En effet, i n’est pas premier puisque p le divise.
Sinon, on passe au nombre premier suivant de la liste, sauf que :
1) si p > √i, on peut conclure que i est premier. En effet, tous les nombres premiers plus petits que sa racine carrée ne le divisent pas.
2) si p = k, on peut aussi conclure que i est premier. k est le plus grand des nombres premiers strictement plus petits que i. i n’a donc pas de diviseur.
Le théorème de Bertrand nous permet d’améliorer cet algorithme.
En effet vérifier la condition 2) est inutile. Comme i < 2k, √i < k. La liste contient donc toujours un nombre premier plus grand que √i : La condition 1) se produit toujours avant la condition 2).
« Je sais que les nombres sont beaux. S’ils ne le sont pas, rien ne l’est. » Surnommé l’homme qui n’aimait que les nombres, Paul Erdös, disparu en 1996 à 83 ans, était hongrois, surdoué et quelque peu excentrique. Il a parcouru le monde, d’université en centre de recherche, stimulant partout où il passait la créativité mathématique. Cosignataire de plus de 1 500 articles sur les sujets mathématiques les plus divers, il faisait mine de dormir aux conférences les plus sérieuses. En lien avec la période historique tourmentée qu’il avait traversée, et qui n’avait pas épargné sa vie personnelle, il manifestait par des aphorismes un pessimisme universel, auquel seul l’univers du nombre, « le seul vraiment éternel », échappait. Il vouait une passion quasi mystique aux preuves « élémentaires », les plus élégantes et les plus courtes, qui selon lui constitueraient le Livre où Dieu aurait consigné les preuves parfaites des théorèmes mathématiques.
… à sa preuve sur ordinateur
Pour l’informaticien, puis l’ordinateur, c’est plus compliqué qu’il n’y paraît. Automatiser la preuve suppose de représenter intégralement le raisonnement dans un formalisme logique compréhensible par l’ordinateur. En outre, dans le cas de l’algorithme de Knuth, qui manipule pourtant des objets mathématiques élémentaires (des entiers), la preuve d’Erdös a mis le système Coq à rude épreuve. L’explicitation de la preuve a en effet nécessité de transformer le problème initial, qui concerne des entiers, en une étude de variation d’une fonction réelle. Et cela n’a pas suffi. En effet, cette étude de variation ne permettait pas de conclure positivement dans tous les cas, mais seulement pour les entiers supérieurs ou égaux à 128. Heureusement, les cas particuliers étaient en nombre fini (126 très exactement : les entiers de 2 à 127). Ils ont dû être traités un à un. Résultat : « Des quelques lignes que représente l’algorithme de Knuth, nous sommes passés à 6 000 lignes de preuve qui en assurent la correction », indique Laurent Théry.
Demain, l’ordinateur mathématicien ?
Plusieurs morales à cette histoire. La première est qu’à un algorithme simple en apparence, peut être associée une preuve formelle très longue et complexe. L’inverse est également vrai, précise Laurent Théry. Est-ce à dire que l’on peut désormais soumettre toute démonstration mathématique à ce traitement ? Dans l’idéal, les informaticiens le souhaiteraient.
La deuxième est que Coq est bien plus qu’un jouet de laboratoire. Des exemples comme celui de l’algorithme de Knuth montrent que ce système de preuves formelles arrive à surmonter cette complexité. « Le fait que nous soyons parvenus assez rapidement à formaliser cet algorithme dans Coq indique que ce système est d’ores et déjà prêt à affronter un large éventail de problèmes réels », prédit Laurent Théry. En particulier, dans des applications dites critiques (transports routiers, aériens…), le système Coq devrait aider à garantir la qualité du logiciel. Autre exemple, cet outil a été utilisé en 2005 par Georges Gonthier et Benjamin Werner pour réaliser une démonstration entièrement vérifiée par ordinateur du théorème des quatre couleurs.
On est toutefois loin de pouvoir s’aventurer sur des démonstrations aussi complexes que celle du théorème de Fermat. La démonstration automatique de théorèmes doit encore faire beaucoup de progrès avant de s’attaquer à une preuve d’une telle complexité. Mais les paris sont lancés. Par exemple, celui de Thomas Hales. Grâce à l’aide des internautes, disposera-t-il d’ici 20 ans d’une preuve formelle de la démonstration de la conjecture de Kepler, qu’il a proposée en 1998 ?
Le mercredi 23 juin 1993, à l’issue de trois jours de conférence, Andrew Wiles concluait en public une présentation de la preuve du Grand Théorème de Fermat. Pour comprendre l’émotion de l’auditoire, il faut revenir plus de trois siècles en arrière. En 1637, Pierre Simon de Fermat (1601-1665), cet érudit et Conseiller du roi au Parlement de Toulouse, énonçait un résultat sur lequel ses successeurs mathématiciens allaient s’arracher les cheveux de génération en génération. Tout simple en apparence, voici cet énoncé : « Si n est un entier supérieur à 2, l’équation Xn + Yn = Zn n’a pas de solution, avec X, Y, Z entiers non nuls ».
Fermat avait affirmé en avoir trouvé une démonstration très élégante, tout en prétextant un manque de place en marge d’un autre texte mathématique pour l’offrir au lecteur.
En juin 1993, personne n’a pu sur le moment vérifier la démonstration de Wiles, dont seules les grandes lignes avaient été exposées oralement. Un comité d’experts de six membres a dû travailler durant des mois pour valider cette démonstration lourde de deux cents pages. À diverses reprises, les experts se sont mis à douter. Ils ont même trouvé un « bogue » dans la démonstration, qui provenait de l’utilisation d’un procédé appliqué hâtivement par Andrew Wiles. Plus de deux ans furent nécessaires pour corriger l’erreur et parvenir enfin à une démonstration complète et acceptée de tous. Avec une preuve formelle, ces tergiversations n’auraient plus lieu d’être.
Est-il vrai que la meilleure façon d’empiler les oranges est l’empilement « pyramidal » (ou en « boulets de canons ») adopté par la plupart des épiciers (on cherche les empilements les plus denses) ?
Présenté par Hilbert, en 1900, lors du congrès international des mathématiciens à Paris, comme l’un des 23 problèmes mathématiques irrésolus les plus « parfaits », les plus faciles à exprimer et les plus difficiles à résoudre (certains ne sont toujours pas résolus aujourd’hui), ce 18è problème est une question bien antérieure, désignée généralement sous le nom de « conjecture de Kepler ». Elle a été formulée en 1611 dans un essai consacré à la cristallographie.
En dimension 2, dans le plan, le problème se ramène à l’empilement de disques ; il a été démontré en 1910 que c’est l’empilement hexagonal qui est le plus dense.
Dans notre espace géométrique de dimension 3, le problème se ramène à un problème « d’optimisation » qui implique… environ 70 variables. Une solution semble avoir été trouvée, proposée par Thomas Hales en 1998, grâce à l’ordinateur… près de 4 siècles après avoir été posé, et après plusieurs démonstrations fausses malgré des efforts colossaux de plusieurs équipes !
Et dans les espaces de dimensions plus élevées ? C’est-à-dire où en plus de la largeur-longueur-hauteur interviennent d’autres variables comme le temps, ou des caractéristiques quantitatives attachées aux objets que l’on cherche à empiler ? De tels espaces correspondent par exemple à des signaux informatiques ou à des codes.
Dans de tels espaces… le problème est encore à résoudre ! Pas de solution générale, alors les mathématiciens essayent d’approcher la solution pour mieux la comprendre, par des approximations ou en regardant des cas particuliers. On sait dire que la densité de ces empilements est assurément inférieure à une valeur maximale : cette borne « supérieure » a été donnée par Rogers en 1958. On sait aussi donner une borne inférieure grâce à un théorème que les mathématiciens connaissent bien : celui de Minkowsky – Hlawka. On sait encore résoudre ce problème dans le cas particulier d’empilements réguliers et pour des dimensions inférieures à neuf !
Une histoire à suivre…
Les tergiversations des mathématiciens, Thomas Hales les connaît bien. Depuis qu’il a proposé en 1998 une démonstration de la conjecture de Kepler longue et complexe, basée en partie sur des calculs effectués par ordinateur, il a fallu 4 ans à une équipe de 12 spécialistes, mandatés pour vérifier sa démonstration, pour conclure que celle-ci est bonne à 99 %. Quant au 1 % restant, ils ne peuvent en décider. Autant dire qu’en l’état actuel, sa démonstration reste suspecte. C’est pourquoi il a décidé de lancer au 1er janvier 2003 le projet flyspeck, qui pourrait durer 20 ans. Ce projet a pour but de fournir par ordinateur une preuve formelle complète de sa démonstration, en utilisant le système HOL.
(Vous trouverez ici plus d’informations en anglais.)
Mise à jour : le 10 août 2014, Thomas Hales a annoncé que le projet flyspeck avait abouti. À peine plus de 10 ans après son lancement…
Newsletter
Le responsable de ce traitement est Inria. En saisissant votre adresse mail, vous consentez à recevoir chaque mois une sélection d'articles et à ce que vos données soient collectées et stockées comme décrit dans notre politique de confidentialité
Niveau de lecture
Aidez-nous à évaluer le niveau de lecture de ce document.
Votre choix a été pris en compte. Merci d'avoir estimé le niveau de ce document !
