Une preuve sur les nombres premiers  

Un ordinateur, c'est avant tout une machine. Est-il alors bien raisonnable de lui confier des démonstrations ? Voici un exemple propre à convaincre les sceptiques. Il concerne la démonstration formelle d'un algorithme très simple bien connu des arithméticiens, une méthode pour calculer les n premiers 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...

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

Le système Coq a été utilisé pour valider cet algorithme.

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.

… à 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 ?