INFORMATIQUE ET VÉRITÉ MATHÉMATIQUE

Preuves mathématiques classiques avec ordinateur

Si l'ordinateur peut conduire à de quasi-certitudes en dehors de la méthode hilbertienne, il peut aussi produire des preuves mathématiques classiques. Plusieurs cas sont possibles, que nous allons présenter en insistant sur ce qui les distingue.

Certaines techniques de démonstration automatique produisent des démonstrations qu'aucun humain n'avait découvertes sans aide informatique, mais qui, une fois trouvées par la machine, se révèlent relativement simples et contrôlables par un mathématicien sans ordinateur. C'est ce qui s'est passé pour la conjecture de Robbins, qui concerne un jeu d'axiomes pour les algèbres de Boole : restée irrésolue pendant une cinquantaine d'années, elle a été démontrée par une technique entièrement automatique en 1996. La preuve donnée par un programme dû à William McCune de l'Argonne National Laboratory (Illinois) se révéla n'occuper que quelques pages, que n'importe quel mathématicien compétent peut contrôler sans aucune aide informatique.

Dans d'autres cas, cependant, une démonstration, ou une partie de la démonstration d'un résultat important, nécessite l'usage d'un ordinateur, mais le calcul opéré par la machine est si long et si complexe qu'aucun humain ne peut en vérifier l'exactitude. Un exemple récent est celui de la conjecture de Kepler.

En 1998, Thomas Hales proposa une démonstration de cette conjecture qui affirme que la façon la plus dense de ranger des sphères dans l'espace conduit à une densité de π/18^1/2. Malheureusement la démonstration de Hales utilise des calculs informatiques, ce qui rend très difficile sa vérification. Un comité d'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 de travail, a indiqué qu'il n'était certain qu'à 99 p. 100 de la validité de la démonstration, obligeant les éditeurs du résultat à publier celle-ci en précisant qu'ils ne peuvent la garantir. Une telle situation ne s'était pas produite pour le grand théorème de Fermat démontré par Andrew Wiles en 1994 : les experts, après quelques aménagements du manuscrit initial, avaient accepté de garantir sa validité. Doit-on considérer aujourd'hui que la conjecture de Kepler est démontrée ? Nous allons voir que la réponse à cette question ne peut qu'être informatique.

Le dernier cas de figure – qui nous ramènera à la conjecture de Kepler – est le plus intéressant et concerne le fameux théorème des quatre couleurs. Celui-ci affirme qu'il suffit de quatre couleurs pour colorier toute carte de telle façon que deux pays ayant une frontière commune ne portent jamais la même couleur.

Ce résultat, conjecturé en 1852 par Francis Guthrie (1831-1899), fut démontré en juin 1976 par Kenneth Appel et Wolfgang Haken, en partie à l'aide d'un calcul par ordinateur. La preuve a été redonnée plusieurs fois – et même améliorée –, mais elle ne fut jamais rendue suffisamment courte pour qu'un être humain puisse la vérifier sans aide informatique. On se trouvait donc dans la même situation qu'avec la conjecture de Kepler. En décembre 2004, un fait nouveau s'est cependant produit, qui crée une situation sans précédent dans l'histoire des mathématiques : une démonstration formelle complète a été produite par Georges Gonthier, des Laboratoires Microsoft de Cambridge, en utilisant un logiciel appelé « assistant de preuve ».

L'écriture complète d'une démonstration formelle, comme Hilbert le demandait, est un idéal que les mathématiciens se donnent rarement la peine d'atteindre : ils se contentent dans la très grande majorité des cas de preuves informelles. Celles-ci[...]