Abstract : We mean to analyse the framework of the theorem by Appel and Haken for the planar maps problem, in order to study how one exploits computer in this proof.

I. Introduction :

En 1852, un jeune étudiant londonnien, Francis Guthrie, écrivit à son frère Frédéric pour lui soumettre une énigme qu’il avait découvert en essayant de colorier une carte des comtés anglais : “Est-il possible avec seulement quatre couleurs (ou moins) de colorier n’importe quelle carte, de telle façon que deux régions ayant une frontière commune ne soient jamais de la même couleur ?”

Ne parvenant pas à résoudre l’énigme, Frédéric Guthrie en parla à son professeur l’éminent mathématien Auguste De Morgan. Le 23 Octobre 1852, dans une lettre adressée au très célèbre William Rowan Hamilton, De Morgan avouait qu’il n’avait pas progressé. Tel sont les premières mentions historiques du problème des quatres couleurs.

Hermann Minkowski, personnage dominant des mathématiques du XIXe siècle, dit un jour à ses étudiants que l’unique raison pour laquelle ce problème n’était pas résolu était que seuls des mathématiciens de troisième ordre s’y était attaqués ; et il ajouta : “Je devrais pouvoir le démontrer”. Quelque temps plus tard il reconnut tout penaud : “J’ai indisposé le ciel par mon arrogance : ma démonstration est, elle aussi, inexacte”. Comme l’ont remarqué Thomas Saaty et Paul Kainen : “L’un des nombreux aspects surprenants de ce problème des quatre couleurs est que les contributions les plus importantes ont été faites par des gens qui croyaient apporter la solution”.

C’est en 1878 qu’apparut la première référence imprimée à ce problème ; il s’agit d’une lettre de Cayley, publiée par les Proceedings of the London Mathematical Society, et demandant si quelqu’un connaissait la solution. En 1879, Arthur Kempe, avocat membre de la société, publia une démonstration, et le problème parut réglé.

En 1890, Percy Heawood découvrit une erreur dans la façon dont Kempe avait traité les régions pentagonales. Un an plus tard une nouvelle démonstration fut publiée par P. J. Tait mais, J. Peterson y dépista aussi une erreur. Heawood avait remarqué que la méthode de Kempe pouvait être aménagée de façon à démontrer que cinq couleurs suffisent dans tous les cas. Il étudia aussi les problèmes homologues relatifs aux surfaces non planes, et donna une limite supérieure du nombre de couleurs requises, en fonction du nombre de trous de la surface.

La conjecture de Heawood, consistant à supposer que le nombre minimal de couleurs est effectivement égal à cette limite, fut démontré en 1968 par G. Ringel et E. Youngs (grâce à certaines théories combinatoires belles et ingénieuses). Restait encore deux exceptions notables. L’une était la sphère (ou le plan), pour laquelle la valeur quatre établie par Heywood restait hermétique, l’autre était la bouteille de Klein, pour laquelle la limite de Heywwod est sept, alors qu’on sait que la réponse correcte est six. En 1968 on connaissait le nombre de couleurs suffisantes pout toutes les surfaces à l’exception du plan ! Ce cas illustre une tendance parfois regrettable des mathématiciens : celle d’entreprendre un travail considérable sur des généralisations, sans pour autant résoudre le problème original qui a donné naissance à la suite des travaux. Evidemment la généralisation peut faire naître une idée assez intéressante pour tout résoudre, cela arrive relativement souvent, mais cette fois ce ne fut malheureusment pas le cas.

II. Enonciation :

En 1879, Kempe tenta de prouver la conjecture des quatre couleurs en démontrant que toute carte normale contenait une face avec cinq voisines au plus et qu’une face ayant deux, trois, quatre ou cinq voisines était “réductible” en ce sens qu’elle ne pouvait pas se trouver dans une carte minimale planaire 5-chromatique. Mais sa preuve de la réductibilité du pentagone n’est pas valable.

En 1913, Birkhoff généralisa les méthodes de Kempe pour prouver la réductibilité et décrivit des algorithmes applicables à des configurations comportant plus d’une face et pouvant conduire à des preuves de réductibilité pour de telles configurations. A la suite, de nombreux investigateurs ont appliqué ces algorithmes pour démontrer la réductibilité de nombreuses configurarions. Celles-ci ont été utilisées pour prouver plusieurs résultats partiels concernant la conjecture des quatre couleurs ; nous désirons mentionner les suivants (à partir d’ici, nous utilisons la terminologie relative aux triangulations du plan et au coloriage des sommets) :
Un graphe minimal 5-chromatique comporte
(a) au moins un sommet de degré 6 ou 7 (Choinacki, Heesch),
(b) non uniquement des sommets de degré 5 et 7 (Heesch),
(c) au mois un sommet de degré 6 ou un triangle 5-5-5 (Stanick),
(d) au moins 96 sommets (Mayer)
(Chacun de ces résultats a été précédé d’une série de résultats plus faibles que nous ne mentionnons pas individuellement.)

En 1950, Heinrich Heesch déclara publiquement qu’il croyait qu’on pourrait démontrer le théorème des quatre couleurs en trouvant un ensemble inévitable de configurations réductibles. Il pensait qu’il faudrait environ 100 configurations, toutes de tailles raisonnables. H. Heesch et l’un de ses étudiants développèrent un programme informatique pour tester la réductibilité. Comme ses successeurs plus évolués, ce programme n’était pas d’une efficacité totale, en ce sens, que quand le test réussissait, la configuration était effectivement réductible, mais quand il échouait le doute subsistait.

Heesch conjecture qu’une preuve de la conjecture des quatre couleurs pouvait être obtenue par des méthodes semblables à celles utilisées pour l’obtention des résultats (a), (b) et (c) ci-dessus, mais qu’un ensemble plus nombreux de configurations réductibles serait nécessaire. Par la suite, Haken observa que la méthode utilisée par Heesch pour obtenir le résultat (a), méthode que nous désignerons sous le nom de “principe de déchargement” (principal of discharging), pouvait être considérablement amélioré. Ceci conduisit à se demander si un procédé de déchargement amélioré de la même manière pouvait être trouvé en vue de traiter le cas général (celui de triangulation planaire sans restrictions concernant le degré ou le nombre de sommets, etc…). Par la suite Appel et Haken entreprirent une recherche systématique sur cette question : les premiers résultats furent présentés. En vue de démontrer la valeur fonctionnelle de cette méthode, Appel et Haken l’appliquèrent (avec des changements mineurs) au cas spécial de triangulation sans sommets de degré 5 adjacents. Ceci aboutit à un ensemble de 47 configurations “apparemment réductibles”, tel que toute triangulations sans sommet de degré 5 adjacent comporte au moins un membre de cet ensemble. Ici une configuration est dite “apparemment réductible” si :
-(1) la longueur n de son circuit n’excède pas le nombre m des sommets qui en font partie de plus de 4, et-(2) elle ne contient pas un “obstacle à la réduction” (à savoir un “sommet à 4 branches”, un “sommet d’articulation à 3 branches”, ou une “paire 5-5 suspendue”).
Tandis que la condition (1) est fondée sur des considérations générales de probabilité, les obstacles à la réduction de la condition (2) ont été observés par Heesch et indiqués dans une communication privée ; par la suite Stromquist, utilisant les méthodes de Tutte et Whitney les a retrouvé théoriquement (comme les cas particuliers les plus importants d’obstacles plus généraux).

Mayer avait développé la méthode personnelle de déchargement pour en dériver le résultat (d) ci-dessus. Lorqu’il apprit le résultat de Appel et Haken concernant l’ensemble de 47 configurations, il trouva une méthode de déchargement particulièrement adaptée au cas spécial des sommets de degré 5 non-adjacents, permettant de traiter ce cas à l’aide d’un ensemble de 14 configurations réductibles de taille (longueur du circuit périphérique) n <= 14 (tandis que l'ensemble de Appel et Haken contenait des configurations allant jusquà n = 16). Ce traitement est probablement le plus court du cas spécial. Entre temps Appel et Haken avaient continué d’améliorer leur méthode de déchargement applicable au cas général. III. Méthode :

Voici un principe de déchargement fondé sur l’égalité suivante, applicable aux triangulations planaires dont tous les sommets ont un degré au moins égal à cinq (nous avons vu plus haut que les sommets de degré <= 4 ont été réduits par Kampe) : Σ((6-i)p_i,i&ge 5)=12 (1)où p_i est le nombre de sommets de degré i. On définit la charge initiale d’un sommet comme étant égale à k(6-i), k étant un facteur choisi pour la commodité de la démonstration, par exemple 10 ou 60.

La charge d’un sommet est positive si i = 5 nulle si i = 6 négative si i >= 7 (sommets majeurs). On définit une méthode de déchargement (discharging procedure) selon laquelle on fait passer les charges positives sur les sommets chargés négativement. Le but de cette redistribution des charges est d’obtenir l’alternative suivante :

(i) aucune des charges modifiées n’est positive, ce qui contredit l’égalité (1) ;
(ii) la triangulation contient une sous-configuration réductible qui n’est pas minimale.

La non-existence des graphes minimaux entraîne comme conséquence logique la non-existence des graphes planaires 5-chromatiques.

Ayant à démontrer le théorème en trouvant un ensemble inévitable de configurations réductible, il semblait que le seul instrument qui pouvait être utilisé pour trouver un tel ensemble inévitable devait être un procédé de déchargement.

Les procédés de déchargement précédemment utilisés dans la démonstration de quelques théorèmes particuliers n’étaient certainement pas assez fins ; une grande quantité d’informations à propos des voisinnages des sommets déchargés et récépteurs était nécessaire pour choisir la charge à transférer. En outre, Appel et Haken ne savaient pas si ce procédé exigeait une seule opération ou plusieurs opérations successives de déchargement. Un second problème était la difficulté de trouver si une configuration est réductible ou non. Lorsque quelques spécialistes eurent fait de grands travaux en détérminantla réductibilité de configurations de taille jusqu’à 9 ou 10, il est apparu qu’un grand nombre de configurations de plus grande taille demandait l’emploi d’un ordinateur.

D’abord Appel et Haken ont cru que des configurations de taille au moins 18 pouvaient être nécessaires. Mais le temps de calcul et l’emmagasinage de l’information sont multipliés par 4 à chaque augmentation de taille et ils ont estimés que quelques uns de ces calculs pouvaient être très difficiles. Par exemple un calcul utilisant un grand ordinateur rapide pour démontrer qu’une configuration particulière de taille 14 n’était pas D-réductible, prenait 26 heures en employant une grande partie de la mémoire centrale. La taille 18 amènerait à multiplier ces nombres par 256 (par exemple) et les problèmes deviendraient alors trop difficiles.

Une méthode pour décider de la solubilité du problème était de chercher des ensembles inévitables de configurations sans obtacle à la réduction. Cette idée semblait raisonnable parce que chaque configuration réductible connue est sans obstacle et que les configuration sans obstable surtout celle dont la longueur n du circuit séparateur n’excède pas le nombre m de sommets qui en font partie de plus de quatre, s’étaient révélées réductibles en général.

En outre, il est très facile de reconnaître si une configuration est sans obstacle. La méthode comportait un rique. On pouvait éventuellement obtenir des ensembles inévitables de configurations sans obstacle comportant des configurations irréductibles qu’on ne pouvait pas éliminer.

Appel et Haken ont choisi de chercher à déterminer un ensemble inévitable de configurations “géographiquement bonnes” (à savoir sans sommets à quatre branches ni sommets d’articulation à trois branches). Ils ont utilisé un programme d’ordinateur pour examiner une classe de procédés de déchargement afin de trouver quelles parties des procédés étaient les plus critiques et quelles valeurs de déchargement étaient les meilleures. Après environ une année, ayant démontrer l’existence d’un ensemble inévitable de configurations géographiquement bonnes, ils ont décidé qu’il était raisonnable de tenter quelque chose de plus difficile. Ils ont modifié le programme afin qu’il leur permette d’obtenir un ensemble inévitable de configurations apparement réductibles (géographiquement bonnes, sans paires 5-5 suspendues et satisfaisant à n – m <= 4). Vers la fin de 1974 il leur apparut qu'on pouvait construire un ensemble inévitable de configurations apparement réductibles de moins de 10 000 membres, et de taille maximale voisine de 16. En outre une grande partie d'un tel ensemble doit avoir une taille inférieure à 15. Ainsi ils ont commencé l'attaque du grand problème. Bien qu’il y eut des programmes d’ordinateur pour prouver la réductibilité des configurations ils ont décidés d’en construire de nouveaux. Ils l’ont fait parce qu’ils ont voulu des programmes qui seraient très efficaces utilisant les ordinateurs de leur Université et parce qu’ils ont eu des idées pour de nouvelles méthodes de C-réduction par ordinateur en cas de besoin. En collaboration avec le Dr. John Koch, qui était à cette époque l’étudiant de Appel à l’Université d’Illinois, ils ont écrit des programmes pour faire des épreuves de D-réductibilité sur des configurations de taille entre 11 et 14. Les programmes, quand ils avaient trouvés qu’une configuration était D-irréductible, faisaient quelques essais pour prouver qu’elle était C-réductible. Avec leur ordinateur le plus rapide (IBM 370-168) le programme pour la taille 14 nécessitait 6 minutes pour les configuration les plus faciles à réduire et moins de 15 minutes pour un grand nombre des autres. Il est important de noter que le procédé est défini à chaque pas après avoir examiné si Appel et Haken pouvaient réduire la configuration ou non. Ainsi ils peuvent établir des critères pour décider quelles configurations accepter. Par exemple, ayant découvert que les configurations de taille 15 ou plus ne semblaient pas nécéssaires, ils les ont rejetées. De plus, si le programme de réduction n’avait pas décidé la réductibilité d’une configuration de taille 14 dans un délai de trente minutes sur l’ordinateur IBM 370-168, ils la considèrent comme irréductible. Ainsi il y a plusieurs configurations théoriquement réductibles que leurs méthodes ont rejetées. Le fait que le procédé a réussi indique que d’autres méthodes semblables (par exemple avec des déchargements T, S, L différents) réussiraient aussi. Ils croient qu’il est possible de produire par ces méthodes un ensemble inévitable d’environ 1000 configurations. Entre 1972 et 1974 Appel et Haken avaient donc entrepris un dialogue interactif avec l’ordinateur. IV. Ordinateur

Le premier essai de leur programme informatique donna une quantité d’informations utiles. Il y avait des éléments positifs : la taille annulaire vraisemblable n’était que 16, et la taille d’un ensemble inévitable était également plus faible que prévu. Il y avait aussi des difficultés : le volume d’informations à extraire de l’ordinateur était prohibitif et la méthode comportait certaines imperfections. Grâce à ces renseignements ils améliorèrent leur programme et firent une nouvelle tentative. Des problèmes plus subtils apparurent, qu’il fallut également résoudre. Après 6 mois environ de ce dialogue, Appel et Haken acquirent la conviction que leur méthode de démonstration de l’inévitabilité avaient de grandes chances d’aboutir. Il fallut un an de plus pour en être tout à fait sûr. En 1975, après avoir une fois de plus encore modifié le programme ils écrivaient :

“A ce moment le programme commenca à donner des résultats surprenants. Au début, nous vérifiions à la main ces arguments, de façon à prévoir son comportement dans toutes les situations possibles ; puis tout à coup il commença à se comporter comme une machine à jouer aux échecs. Il combinait des stratégies fondées sur tous les trucs qu’on lui avait appris, et souvent ces méthodes s’avéraient plus efficace que celles que nous aurions spontanément utilisées. Il commenca ainsi à nous faire découvrir des procédés innatendus. En un certain sens il avait dépassé ces créateurs pour les tâches intellectuelles et pour les tâches mécaniques.”

D’après Haken : “D’un bout à l’autre du calcul n’importe qui peut étudier et vérifier chaque détail. Le fait qu’un ordinateur puisse traiter en quelques heures plus de cas particuliers qu’un humain ne pourrait espérer le faire dans toute sa vie ne change rien au concept même de démonstration. Ce qui a changé ce n’est pas la théorie c’est la pratique des mathématiques.”

Mais Appel et Haken sont convaincus pas des analyses probabilistes qu’un ensemble inévitable beaucoup plus petit et contenant des configurations de beaucoup plus petite taille n’existe pas. Ils ont employé 1000 heures de temps d’ordinateur à prouver la réductibilité des 1880 configurations de leur ensemble. Ils croient qu’il est possible de produire un ensemble qui exigent seulement 200 heures pour la vérification. Mais ils sont sûr qu’il est impossible de produire une telle preuve vérifiable à la main. Jean Mayer, un des très grands experts du monde 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, il faudra admettre que le théorème des quatre couleurs exige une preuve que persone ne peut vérifier sans ordinateur 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 coloriage mis en jeux : 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éfléchissons un peu plus 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 disymétrique. Le problème est de trouver le plus petit nombre possible de couleurs tel que la propriété soit vérifiée. Comme on l’a vu précédemment 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 nous avons vu qu’il n’était pas trivial de prouver 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 (l’indice). 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ématiqe – c’est d’ailleurs l’unique création de l’homme qui atteigne l’infini ! (On a d’ailleurs le même genre de finitisation pour la conjecture de Catalan grâce au résultat de Terjanian qui a été rendu explicite par Langevin ).

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 lorqu’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 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, 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 quatre couleurs cette dernière tentative a échoué et l’on s’est retrouvé avec un résultat démontré grâce à l’ordinateur. Signalons à ce propos que les spécialistes omettent volontairement ou non de souligner la part heuristique jouée par l’ordinateur dans ce problème ; nous espérons d’ailleurs qu’avec notre article nous avons effectué une mise au point à ce sujet.

Ensuite lorsque l’on se trouve dans la situation où l’ordinateur a été indispensable, 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 quatre 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étodes trop proches pour résoudre le cas général.

C’est à ce niveau-là que nous prenons le contre-pied de la position habituelle et majoritaire de mathématiciens. Nous nous plaçons dans la problématique qu’aurait eue un épistémologue pregö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 !

A notre époque certains mathématiciens s’acharnent à trouver des démonstratins 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 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 20e 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 15 000 pages !! (Précisons à son propos que ce résultat est objectivement plus contestable que le théorème des quatre couleurs puisque plus sujet à l’erreur étant donné l’importance du rôle social entre les mathématiciens. Alors qu’aucun mathématicien n’émet de doute quant à la validité de sa preuve. Comme quoi le jugement des mathématiciens est extrêmement subjectif malgré la prétendue appartenance de leur domaine au monde des idées.) Mais que ce serait-il passer 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 ? (comme c’est le cas avec P_12 qui est égal à 1 104 891 746 ni plus ni moins !)

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’auto-référence est souvent au rendez-vous.

V. Conclusion

Pour finir essayons d’expliciter ce que nous avons voulu démontrer tout au long de ce cycle “DEMONSTRATION” constitué de quatre parties.
Au cours de ces chapitres nous avons examiné des problèmes où le rôle de l’ordinateur était croissant ce qui nous a amené à considérer le problème de la vérificatin qui lui-même nous a conduit à l’un des deux paramètres fondamentaux de la notion de démonstration à savoir la longueur, l’autre étant la complexité.

Par ailleurs 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 cette possibilité et dans certains cas – comme celui du théorème des quatre couleurs – l’on n’arrive pas à prouver la vérité d’une conjecture.

Donc le rôle singulier du théorème des quatre couleurs n’a pas fini d’ennuyer la communauté des mathématiciens classiques bien au contraire car une fois son aspect générique mis en place, comme nous le prédisons, il montrera du même coup la puissance du trio infernal : Axiom of Choice, Axiom of Continuum, Axiom of Computer.

Ainsi nous aurons effectivement la preuve qu’il n’y a pas de voie royale en Mathématiques, sur le chemin de la Connaissance il y a de nombreux carrefours et donc la richesse d’un parcours dépendra du choix du chercheur qui aura sans cesse dans l’encéphale le fait que choisir c’est se priver !

Bibliographie

K. Appel, W. Haken : Every planar map is four colorable. Part I : Discharging. p. 429-490.

K. Appel, W. Haken, J. Koch : Every planar map is four colorable. Part II : Reducibility. p. 491-567, Illinois Journal of Mathematics Vol. 21 n° 3 (Issue 84), sept. 1977.

K. Appel, W. Haken : An unavoidable set of configurations in planar triangulations. J. of Comb. Th. Series B26, p. 1-21, 1979.

K. Appel, W. Haken , J. Mayer : Triangulation à v_5 séparés dans le problème des quatre couleurs. J. of Comb. Th. Series B27, p. 130-150, 1979.

J. Mayer : Un nouveau type de preuve mathématique : le théorème des quatre couleurs. I- Exposé préliminaire. p. 67-80

K. Appel : Un nouveau type de preuve mathématique : le théorème des quatre couleurs. II- Le théorème des quatre couleurs. p. 81-88, Publ. du dép. de Math. Lyon t.16-3.4, 1979.

I. Stewart : Les mathématiques. (Chap. Le théorème des quatre couleurs. p. 117-126). Belin 1989, Oxford 1987.

E. R. Swart : The philosophical implications of the four-color problem. Amer. Math. Monthly 87, p. 697-707, nov. 1980.

T. L. Saaty, P. C. Kainen : The four-color problem. Assaults and conquests. Mc. Graw-Hill, (ix + 217 p.), 1977. (#MR 58 246, by W.T. Tutte).

K. Appel, W. Haken, with the collaboration of J. Koch : Every planar map is four colorable. Contemporary Mathematics 98, Amer. Math. Soc., (xvi + 741 p.), 1989. (#MR 91m : 05 079, by F. Bernhart).