Depuis la parution des Éléments de mathématique de Nicolas Bourbaki, l’ordinateur a fait son apparition dans l’univers mathématique. Il sert même dans des démonstrations qui sont trop longues et complexes pourqu’on les vérifie à la main. Cet avènement impose une remise en question de la notion de preuve.

Démonstrations par l’ordinateur

En 1998, Thomas Hales proposa une démonstration de la conjecture de Kepler qui indique que la façon la plus dense de ranger des sphères dans l’espace est celle des empilements des boulets de canon¹ et conduit à une densité de $\pi/\sqrt{18}.$ Malheureusement, une partie de la démonstration de Hales utilise des calculs informatiques, ce qui rend très difficile sa vérification pas à pas.

La démonstration de Hales a été publiée dans le prestigieux journal The Annals of Mathematics. Un comité de douze experts présidé par le mathématicien Gabor Fejes Toth (spécialiste des problèmes d’empilements) a été chargé d’examiner la validité de la preuve. Ce comité, malgré quatre années d’un travail acharné, a indiqué qu’il n’était certain qu’à 99 pour cent de la validité de la démonstration. Le journal a donc publié la preuve avec cette réserve. Une telle situation ne s’était pas produite pour le grand théorème de Fermat, démontré par A. Wiles il y a bientôt une douzaine d’années, et dont les experts, après quelques aménagements du manuscrit initial, avaient accepté de garantir la validité de la preuve.

Pour remédier à la situation nouvelle créée par la démonstration de Hales, un projet intitulé Flyspeck a été engagé. Son but est de contrôler à l’aide de techniques informatiques chaque pas de la démonstration, ce qui revient à écrire explicitement une preuve formelle comme celles envisagées par Hilbert ou Bourbaki². Le projet demandera 20 hommes-années de travail pour être mené à terme. Seules la longueur et la complication inhabituelles de la preuve de Hales rendent obligatoire l’utilisation de telles méthodes pour garantir une preuve et certains y voient une nouvelle ère pour les mathématiques.

Je voudrais insister sur un exemple plus net encore de l’intrusion brutale des ordinateurs en mathématiques. Le livre paru en 2003 de Steven Finch intitulé Mathematical Constants est une encyclopédie de 600 pages consacrée aux constantes mathématiques. Le livre s’intéresse bien sûr aux grandes vedettes que sont \(\pi\) et e, mais aussi à plusieurs centaines d’autres constantes rencontrées dans toutes sortes de domaines mathématiques. Il se termine par une table donnant la valeur approchée d’un millier de constantes. Les valeurs numériques citées aussi dans le texte de l’ouvrage et dans cette table doivent être vues comme des théorèmes, chacun de la forme:

La constante de Catalan,
la somme de la série:
1–1/32+1/52–1/72…
vaut 0,9159655941…

Ces centaines de théorèmes, qui constituent une part importante du contenu de l’ouvrage, ont, sauf quelques-uns, été démontrés à l’aide d’un ordinateur. Bien sûr, les étapes de ces démonstrations – ici des calculs, ne sont pas détaillées – dans l’ouvrage ni n’ont été contrôlées à la main³.

Le livre de Finch contient donc plusieurs centaines de propositions dont les preuves reposent sur les ordinateurs. L’usage des preuves par ordinateur n’est donc pas rare et dans bien des cas n’émeut plus les mathématiciens. Ceux qui formulent des doutes sur l’acceptabilité des preuves mathématiques par ordinateur et qui soutiennent que seuls les théorèmes mathématiques provenant d’un travail humain, ou humainement vérifiable, doivent être considérés comme authentiquement prouvés, devraient aussi s’interroger sur ce cas.

Il semble ainsi que la notion de preuve acceptable évolue et qu’en pratique aujourd’hui elle tolère l’usage d’un calcul par ordinateur. Bien plus, dans certains cas, il semble que seul l’ordinateur pourra valider un résultat que les humains, trop faillibles, proposent. Cette acceptation de l’ordinateur pour fonder certaines certitudes mathématiques repose toujours sur la notion de preuve formalisée que Hilbert défendait. Cependant, d’autres pratiques récentes montrent que l’informa- tique remet en question plus profondément l’idée que seule une preuve classique et formalisable produit de la certitude mathématique.

Démonstrations probabilistes

Il arrive qu’une erreur se glisse dans une démonstration et qu’elle passe inaperçue pendant des décennies. Cela s’est produit pour le théorème des quatre couleurs dont aujourd’hui on ne connaît que des preuves utilisant l’ordinateur (voir encadré à la page 23). Aussi, la probabilité qu’une preuve un tant soit peu complexe soit fausse n’est jamais totalement nulle: donc, même au sens classique, une preuve peut n’apporter qu’une certitude forte et jamais absolue (faire vérifier la preuve par un ordinateur ne réduit pas le risque à zéro, car les mêmes erreurs de raisonnement peuvent être présentes dans les logiciels utilisés).

Il en résulte que si certaines vérités mathématiques étaient connues avec un risque d’erreur très faible, nous devrions les considérer comme aussi certaines que les théorèmes prouvés par des démonstrations classiques (avec ou sans ordinateurs). Il se trouve que, depuis 1975, le problème se pose vraiment, car des méthodes de preuves probabilistes ont été introduites par les mathématiciens M. Rabin et G. Miller pour établir qu’un nombre est premier. Ces méthodes permettent d’engendrer des nombres entiers dont on sera certain, par exemple à 99,9999999 pour cent, qu’ils sont premiers. Si un risque de $1/10^9$ vous paraît trop important, paramétrez votre méthode de preuve probabiliste pour qu’il soit de $1/10^{12}$ ou $1/10^{20},$ mais ne soyez pas trop exigeant et n’oubliez pas que, selon votre âge, la probabilité que vous avez de mourir dans la prochaine seconde varie entre $1/10^9$ et $1/10^{11}$. Or, aujourd’hui, malgré la découverte en 2002 d’un algorithme fonctionnant en temps polynomial pour prouver la primalité, les méthodes les plus efficaces pour établir qu’un nombre est premier sont probabilistes: ce sont donc elles qu’on utilise en cryptographie lorsqu’on a besoin de grands nombres premiers. En pratique donc, faisant fi des réticences des mathématiciens qui prétendent que seules les preuves traditionnelles produisent de la certitude, les cryptologues utilisent massivement les preuves probabilistes.

De plus, les logiciels de calcul symbolique (Maple, Mathematica, etc.) se servent de ces méthodes dès qu’on les interroge sur des nombres ayant beaucoup de chiffres. Toutefois, même lorsqu’une preuve est probabiliste, elle reste communicable: en transmettant les éléments à votre disposition qui vous ont persuadé qu’un certain nombre N est premier avec un risque P d’erreur, vous persuaderez votre interlocuteur que N est premier avec un risque P d’erreur.

Conviction incommunicable

Cette transmissibilité de la certitude — jugée essentielle par beaucoup de mathématiciens — n’est pas une règle absolue, car un type de preuve, inventé il y a 20 ans par les trois mathématiciens O. Goldreich, S. Micali et C. Rackoff, conduit à des certitudes non partageables. Les preuves « sans transfert de connaissance »⁵ permettent à quelqu’un d’acquérir la certitude qu’un énoncé mathématique E est vrai sans pourtant qu’il dispose d’aucune information communicable lui permettant de faire partager à un tiers sa conviction de la vérité de E.

Le principe général des preuves sans transfert de connaissance est le suivant:

– Alain dispose d’une information de type mathématique, par exemple qu’une carte est coloriable en utilisant trois couleurs seulement (ce qui n’est pas évident puisque le théorème déjà évoqué indique seulement que quatre couleurs suffisent).

– Alain dialogue avec Béatrice d’une telle façon qu’il la persuade qu’il connaît un coloriage à trois couleurs et donc qu’un tel coloriage existe bien. Pourtant, le dialogue ne permet pas à Béatrice d’acquérir la moindre information sur le coloriage détenu par Alain.

– Après l’échange, Béatrice se trouve donc dans la situation suivante: elle a la certitude que la carte est bien coloriable avec trois couleurs, mais ne sait pas faire un tel coloriage et elle ne peut communiquer sa certitude à personne.

Avec ce type de schéma — utilisé en cryptographie pour concevoir des protocoles d’authentification — on découvre donc qu’une certitude mathématique, comme celle de Béatrice, peut être incommunicable⁶.

Démonstrations quantiques

L’idéal classique des démonstrations claires, sans risques, communicables et vérifiables par tous est bien loin. Cependant, le pire n’est peut-être pas atteint, car le calcul quantique pourrait dans l’avenir conduire à des situations encore plus étranges. Dans le cas du coloriage à trois couleurs, un personnage de l’histoire (Alain) possède une preuve communicable. Même si Béatrice a acquis la certitude du résultat sans prendre connaissance de la preuve classique, la preuve classique existe quelque part et quelqu’un la connaît.

Avec les preuves quantiques, tout cela pourrait bien changer. L’idée du calcul quantique est d’opérer simultanément un grand nombre de calculs en parallèle en exploitant les superpositions d’états que permet la mécanique quantique. Par nature, les étapes d’un calcul quantique ne sont pas accessibles: en prendre connaissance perturberait le déroulement du calcul et le fausserait. Si un résultat mathématique était démontré par un ordinateur quantique, il se pourrait donc qu’on ne dispose pas des étapes de calcul ayant conduit au résultat. Nous serions donc dans une situation où « quelque chose » aurait prouvé le résultat, nous l’aurait communiqué, mais sans rien nous transmettre des arguments ayant conduit à celui-ci. Comme dans le cas d’Alain et Béatrice, nous aurions la certitude de la validité d’un résultat (pour peu que notre machine soit fiable), mais ici ni Alain, ni personne ne détiendraient d’éléments tangibles constituant la preuve: nous aurions acquis une certitude mathématique sans que le moindre élément de preuve ne subsiste.

Une telle situation, envisagée récemment par C. Calude, E. Calude et S. Marcus, ne s’est pas encore produite, mais si un jour nous réussissons à mettre au point des ordinateurs quantiques et que nous les utilisons pour démontrer des résultats mathématiques, dans certains cas nous nous trouverons donc avec la certitude nue qu’un énoncé est vrai.

On le voit, tant que l’être humain n’a utilisé que le crayon et le papier pour faire des mathématiques, la notion de démonstration n’a pas posé de problèmes graves, même dans le cas des preuves sans mots⁷ qui, par jeu, apparaissent imprécises et risquées. Depuis que les ordinateurs, quantiques ou non, sont entrés dans la danse, tout est devenu plus compliqué, et il semble qu’existent maintenant des certitudes mathématiques de natures différentes. L’homme, en s’aidant des systèmes matériels complexes pour explorer le monde abstrait, se trouve avec lui dans un rapport nouveau, plus riche et plus varié qu’auparavant.

Pour en s\(\alpha\)voirplus !

FINCH, Steven. Mathematical Constants, Cambridge Univ. Press, 2003.
CASSELMAN, Bill. On the dissecting table, + PLUS magazine, 25, mai 2003.
GOLDREICH, Oded. Zero-Knowledge Twenty Years After Its Invention. Dec. 2002.

Sur la démonstration de la conjecture de Kepler par Hales et le projet Flyspeck
http://www.math.pitt.edu/~thales

Sur les preuves sans transfert de connaissances
COURTOIS, Nicolas. Comment tout dire sans rien révéler, Dossier La cryptographie, Pour la science, 2002, pages 54-57.
CALUDE, Christian, Elena CALUDE et Solomon MARCUS, Passage of Proof, mars 2003. Voir:
http://arxiv.org/abs/math/0305213
NELSEN, Roger. Proof without words, in The Mathematical Association of America, Tome I, 1993, Tome II, 2000.
ALSINA, Claudi et Roger NELSON. Math made visual. MAA, 2006.

DELAHAYE, Jean-Paul. Merveilleux nombres premiers, Belin-Pour la science, Paris, 2000 (Sur les preuves probabilistes de primalité, voir le chapitre 8).
MASHAAL, Maurice. Bourbaki, une société secrète de mathématiciens, Collection Les génies de la science, Pour la science, 2000.

PDF