Considérons le principe suivant. Si un théorème dépend de toute la structure de l’objet étudié, alors, pour rendre son utilisation effective il faudra sans doute l’ordinateur. Il est bien évident que la véracité de ce principe dans le cas général est contestable, pour le voir il suffit de considérer un problème qui ne concerne que peu d’objets. Par contre si l’on a affaire à un grand nombre d’objets et s’ils sont un tant soit peu compliqués, alors, la puissance du principe devient flagrante. De sorte qu’il est préférable de l’énoncer sous une forme plus précise – mais un peu plus formelle. Si une démonstration d’un théorème sur n objets (pour n suffisamment grand mais fini) nécessite l’utilisation d’un théorème qui dépend de toute la structure (suffisamment complexe) des objets auxquels il s’applique alors l’ordinateur sera nécessaire à sa réalisation.Il semble que l’on puisse aller encore plus loin dans cette idée en augmentant soit le nombre n d’objets soit leur complexité car alors on en arrive à l’énoncé qui est inaccessible même à l’aide de l’ordinateur, du moins dans sa totalité. Par exemple l’on pourrait se retrouver dans la situation suivante qui représente bien sûr un cas particulier du précédent principe. Si le problème général est indécidable alors le problème partiel rend l’ordinateur indispensable. Il est bien évident qu’en se restreignant à des préoccupations générales comme nous l’avons fait l’on ne saurait obtenir comme résultat autre chose que des principes. De toute façon le but que nous désirons atteindre ici n’est pas de construire une théorie complètement axiomatisée du rôle de l’ordinateur au sein de la théorie de la démonstration. Nous nous contentons seulement, du moins pour l’instant, d’écrire les prémices de cette théorie de la démonstration.

En ce qui concerne le théorème des 4 couleurs Appel et Haken sont convaincus par des analyses probabilistes qu’un ensemble inévitable beaucoup plus petit et contenant des configurations de beaucoup plus petite taille n’existe pas. De récents développements dans la démonstration du théorème des 4 couleurs qui ont simplifié la partie traitée par l’humain et non par l’ordinateur vont dans ce sens. Appel et Haken ont employé 1000 heures de temps de calcul à prouver la réductibilité des 1880 configurations de leur ensemble. Ils croient qu’il est possible de produire un ensemble qui exige seulement 200 heures pour la vérification. Mais ils sont sûrs qu’il est impossible de produire une telle preuve vérifiable à la main. Jean Mayer, un des grands experts en matière de réductibilité, ne croit pas que la tâche de vérifier un tel ensemble à la main soit praticable. Ainsi, si personne ne trouve une preuve plus simple sans utiliser d’ordinateur, il faudra admettre que le théorème des 4 couleurs exige une preuve que personne ne peut vérifier à la main même en y passant toute sa vie.

La solution exige une étude combinatoire d’autant plus complexe que les données logiques sont plus simples et peu susceptibles d’engendrer des théorémes généraux. Pour les mêmes raisons, l’ensemble inévitable de configurations réductibles ne peut se réduire à un petit nombre d’éléments. Enfin, la plupart des réductions auxquelles on aboutit sont impraticables à la main, vu le grand nombre de coloriages mis en jeu : on voit donc en quoi la démonstration du théorème, quoiqu’accessible à notre logique, dépasse par son ampleur les capacités de l’intelligence individuelle.

Elle illustre l’avènement d’un nouveau type de preuve mathématique. En effet, c’est la première fois, à notre connaissance, qu’un théorème impliquant par sa nature un nombre infini de cas se trouve ramené à une étude combinatoire finie, mais d’une ampleur telle que la preuve a nécessité plusieurs centaines d’heures d’ordinateur et que, même a posteriori, une vie d’homme ne suffirait pas à la rendre explicite.

Réflechissons un peu sur ce dernier point et analysons l’idée sur laquelle il est basé. Tout d’abord le problème initial concerne deux infinités, le nombre de cartes et le nombre de couleurs, qui ont bien sûr un rôle dissymétrique. Le problème est de trouver le plus petit nombre possible de couleurs tel que la propriété soit vérifiée. Il est trivial de montrer que ce nombre est supérieur ou égal à 4 et il est facile de montrer que ce nombre est inférieur ou égal à 5. Il s’agit donc d’un problème où l’on peut aisément obtenir une borne supérieure et une borne inférieure de la valeur recherchée. Par contre il n’est absolument pas trivial de montrer que la valeur est précisément 4. Pourquoi une telle différence de complexité ? Du point de vue théorique il est naturel que la minoration soit plus facile à obtenir puisque somme toute il ne s’agit que de trouver une carte qui nécessite un nombre donné de couleurs pour la colorier. Par ailleurs dans le cas présent la facilité d’obtenir une majoration provient non pas d’un raisonnement symétrique mais des contraintes imposées sur le graphe associé à la carte considérée par la formule d’Euler. Ainsi pour la valeur recherchée, la difficulté consiste bien à prouver l’égalité avec l’une des deux bornes, seulement ce problème concerne une infinité de cartes même en les traitant à isomorphie près. La méthode utilisée, du point de vue de la mathématique pure, va consister à rendre fini le nombre de cartes à étudier. Ce passage de l’infini au fini représente une étape fondamentale ; c’est sans aucun doute l’une des situations où l’on peut le mieux prendre conscience de la puissance de l’outil mathématique.

Une fois cette étape cruciale franchie un autre problème apparait : le nombre de cas à traiter. Bien sûr si ce nombre est très petit, la gêne causée devient dérisoire. Mais qu’en est-il lorsqu’il est grand ? S’il est vraiment très grand et qu’il appartient aux nombres métaphysiques comme dirait F. Le Lionnais, l’on ne peut guère en dire quoi que ce soit puisqu’il est par définition inaccessible à toute méthode raisonnable. Par contre si ce nombre est accessible, cela dépend bien sûr du problème, et alors plusieurs difficultés méthodologiques apparaissent :

Tout d’abord comment faire pour réduire ce nombre ? Dans les cas les plus favorables il faut réitérer la méthode, cependant ils ne représentent pas la majorité. Dans les cas plus difficiles seul le changement de la méthode utilisée permet de réduire ce nombre. Mais dans les cas les plus difficiles on ne sait pas faire mieux, alors si cela est possible on fait appel à l’ordinateur. Ce qui a pour conséquence directe de donner un rôle important à ce dernier. Si celui-ci permet d’obtenir un contre-exemple, son rôle est effacé et l’on n’en parle plus que laconiquement. S’il permet de compléter la démonstration du théorème conjecturé alors dans un ultime effort l’on essaye a posteriori et en utilisant les résultats de ses calculs d’éliminer sa contribution. Pourtant dans le cas du théorème des 4 couleurs cette dernière tentative a échoué et l’on s’est retrouvé avec un résultat démontré grâce à l’ordinateur.

Ensuite lorsque l’on se trouve dans une situation où l’ordinateur a été indispensable, l’on est en droit de se demander si en utilisant une autre méthode (dans le futur) il aurait encore été nécessaire. En ce qui concerne le problème des 4 couleurs on sait grâce aux analyses probabilistes d’Appel et Haken que des variantes de la méthode utilisée seraient obligées d’employer l’ordinateur. Seulement cela n’est pas convaincant car il s’agit de méthodes trop proches pour résoudre le cas général.

C’est à ce niveau là que nous prenons le contre-pied de l’opinion majoritaire. Nous nous plaçons dans la problématique qu’aurait eue un épistémologue prégödelien fictif. Car si à l’époque de Gödel les mathématiciens n’ont point trouvé son théorème, cela ne provient pas tellement de la difficulté technique mais plutôt conceptuelle. En fait de façon plus concise l’on peut dire qu’ils ne réfléchissaient pas au bon problème. Ils s’étaient tous mis dans l’idée de chercher à unifier les mathématiques en les ramenant à une structure dont ils espéraient démontrer la cohérence sans se poser un seul instant la question de savoir si cela était seulement possible !

À notre époque certains mathématiciens s’acharnent à trouver des démonstrations où l’intervention de l’ordinateur est éliminée. Mais après tout il ne peut s’agir là que d’un acte de foi car l’on ne sait pas si cette procédure est possible dans le cas général.

Car de la même façon que l’on ne peut lutter contre les lois physiques, l’on ne peut guère lutter contre un fait mathématique (comme c’est le cas lorsque l’on a affaire à des structures indépendantes). Par exemple une des grandes réussites du 20ème siècle sur le plan mathématique a été la classification des groupes finis simples et donc aussi l’explicitation des groupes sporadiques, l’oeuvre de nombreux mathématiciens, qui ont travaillé pendant plusieurs décennies, dont la démonstration comporte actuellement plus de 15000 pages ! Mais que se serait-il passé si au lieu de 26 groupes sporadiques, il y en avait eu 260 ou 2600 ? Car l’esprit humain, et par conséquent les mathématiques qui en sont un des honneurs, a toujours tendance à unifier, à synthétiser les objets qu’il étudie pour mieux les comprendre, mais comment faire s’il y a à faire face à des structures véritablement indépendantes ?

Ainsi si l’on arrivait à démontrer qu’un problème comporte un grand nombre de structures indépendantes on montrerait du même coup la nécessité d’utiliser un ordinateur, si le nombre est accessible évidemment. Pour cela il faudrait montrer que quelque soit la méthode utilisée, la donnée des structures à considérer est incompressible. Peut-être d’ailleurs que le théorème, qui démontrera la nécessité de l’utilisation de l’ordinateur pour démontrer un théorème sera lui-même démontré à l’aide de l’ordinateur ? Après tout lorsque l’on parle de fondements l’autoréférence est souvent au rendez-vous.

Pour finir essayons d’expliciter ce que nous avons voulu démontrer. Nous avons voulu mettre en évidence que du point de vue de la théorie de la démonstration, l’action de l’ordinateur intervenait de la même façon que l’utilisation d’un axiome. En effet l’alternative est simple : soit on utilise l’axiome de l’ordinateur c’est-à-dire que l’on se permet d’employer une procédure mécanique qui détermine si un ensemble fini, mais grand, de cas à considérer vérifie ou pas une certaine propriété, soit on exclut la possibilité et dans certains cas – comme celui du théorème des 4 couleurs – l’on n’arrive pas à prouver la vérité d’une conjecture.