La preuve par l'informatique

C'est en 1611 que Johannes KeplerJohannes Kepler, énonce - sans en apporter la preuve formelle - ce que tout bon marchand de fruits sait d'instinct : la meilleure façon d'empiler des oranges consiste à former une pyramide où chacune d'entre elles repose sur le creux délimité par ses voisines de la couche inférieure. La résolutionrésolution de ce problème exposée par Hales il y a six ans n'avait à l'époque pas convaincu tout le monde car elle reposait en grande partie sur des opérations effectuées par ordinateurordinateur, un instrument dont les mathématiciensmathématiciens se méfient comme de la pestepeste.

Pendant six longues années donc, des correcteurs se sont penchés sur les travaux de l'Américain afin d'en vérifier à la main le moindre résultat. Mais la tâche était titanesque et il a fallu trancher la question de la validité des preuves fournies en dépit des ambiguïtés liées au recours à l'informatique. Les prestigieuses Annals of Mathematics ont ainsi décidé de publier la partie théorique des recherches de Hales, laissant à un journal plus spécialisé, Discrete and Computational Geometry, le soin d'éditer le reste.

Cette décision représente un compromis qui fera date dans l'histoire des débats de plus en plus fréquents qui opposent les mathématiciens partisans de l'ordinateur et ses détracteurs.