2. 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 π/181/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 […]
… pour nos abonnés, l'article se prolonge sur 3 pages…
