Théorème des quatre couleurs.

Bonjour,
Réf. : https://www.maths-forum.com/lycee/les-quatre-couleurs-t214843.html
Ce fameux problème des quatre couleurs a fait couler beaucoup d'encre de toutes les couleurs.
Il a même servi de support à l'affirmation que un théorème peut être démontré par un ordinateur. Je m'explique.
Apparemment, on n'a toujours pas réussi à le démontrer par la logique mathématique.
Alors, on a créé "toutes" les configurations possibles et on a écrit un logiciel qui essaye toutes ces configurations possibles. Au bout de plusieurs heures, le logiciel n'a trouvé aucune impossibilité, donc, on a dit : "l'ordinateur a démontré le théorème des 4 couleurs".

Je me suis intéressé à ce problème il y a quelques années. Il y a eu des articles sur le Web décrivant cela (démonstration informatique). L'article était signé, ancien élève de polytechnique, j'ai essayé de le contacter, la mail était faux. J'ai contacté l'école pour plus de renseignements, cet individus n'était pas connu. Bref, c'était un énorme canular. Toujours est-il que je ne sais toujours pas s'il y a un fond de vérité dans cette histoire de démonstration informatique.
J'ai eu plusieurs échanges à ce sujet avec Sylviel, il semblait très bien informé. Je me suis longtemps demandé si ce n'était pas lui l'auteur du canular.

Bonsoir Dlzlogic,

Intéressant. Non seulement on ne saurait pas si l'ordinateur a vraiment "démontré" ce théorème, mais en plus on ne saurait pas si un ordinateur l'a vraiment fait ? J'avais pourtant entendu parler d'équipes entières de chercheurs (pas des péteux français) qui avaient obtenu ce résultat.

De toute manière, que ce soit par l'homme (son cerveau) ou la machine, c'est toujours un ordinateur qui démontre des théorèmes, non ? Avec souvent les mêmes problèmes de fiabilité...

Oui cette histoire m'a beaucoup occupé.
Ca a commencé par une question sur un forum de géomatique (c'est aussi un de mes centres d'intérêt), quelqu'un voulait une logique (autrefois on appelait ça un algorithme) pour colorier en 4 couleurs un ensemble de zones. C'est là que je me suis renseigné. En fait, l'importance de la démonstration est mineure, sauf pour occuper certains. Donc, en gros, je crois finalement on a effectivement dépensé beaucoup de temps pour "démontrer cela", mais que c'est en fait particulièrement inutile. Par ailleurs je suis sûr qu'il y a un individu qui a monté ce gag avant à un moment ou à un autre.

L'histoire de ce théorème des quatre couleurs m'intéresse parce que, d'une part, j'ai suivi les différentes affirmations depuis le début, cf. le canular lisible avant le moindre article un peu sérieux et aussi à cause de l'intérêt assez limité par rapport aux moyens mis en œuvre et ainsi à la publicité qui en a été faite à l'époque.
Avec le recul, cette démonstration est cité comme un exemple caractéristique d'une démonstration que l'on peut faire avec un logiciel.
Ce que je veux dire par là c'est que je n'ai pas entendu parler d'autre démonstration qu'on ne peut pas faire par la logique mathématique, mais qu'un algorithme, bien codé, peut faire avec une machine.
Il y a bien sur le logiciel Coq qu'on ne manquera pas de citer.
Mais finalement, quel est le but de tout cela ? Je prends l'exemple des 4 couleurs. Indépendamment de la démonstration, ce théorème est vrai. La seule chose intéressante est de savoir colorier un tel ensemble de zones.
Je mets en comparaison des choses plus importantes comme la théorie des probabilités. Dans ce cas, les démonstrations sont parfaitement rigoureuses, c'est à dire qui ne dépendent que d'un postulat et de notions mathématiques élémentaires. Or, il s'avère que cette théorie n'est pas connue, donc, pas admise par un grand nombre de matheux.
Alors, je pose la question : qu'est-ce qui est important, des notions utiles ou une démonstration informatique d'une chose dont personne ne doute ?

Bonsoir,

Merci des précisions Dlzlogic. L'intérêt principal du théorème des quatre couleurs me semble d'avoir détruit le mythe de la preuve mathématique humainement vérifiable sous toutes coutures, donc "infaillible". Malgré ce démenti célèbre, beaucoup de matheux et logiciens continuent à y croire mordicus...

Bonsoir Ltav,
Oui, tout à fait, c'est exactement ça.
Mais, à mon avis, on se trompe de cible. En ce sens que je me demande quel plaisir on peut avoir à démontrer un théorème pour prouver que c'est possible de le démontrer par des méthodes différentes.
Sans aller aussi loin, il y a des problèmes simples, de tous les jours que l'on sait parfaitement mettre en équation pas difficile, mais cette équation, on ne sait pas la résoudre algébriquement. Je fais allusion à la section d'un tuyau en écoulement libre. Dans mon cours (1960) il n'y a pas d'autre méthode que de "recommencer" le calcul. Maintenant, ce type de calcul est réalisé par un logiciel assez élémentaire. Je te rappelle que l'assainissement pluvial est une de mes spécialités.

Bonsoir Dlz, très intéressant. Puis-je voir juste la tête de cette problématique de recommencement de calculs dans ton cours ?

Par rapport au T4C, tu as raison de discuter l'utilité scientifique de rechercher une telle démonstration non-machinisée, mais n'oublie pas le facteur humain de l'orgueil dans cette histoire : beaucoup de matheux scientistes auront tout le mal du monde à admettre que la démonstration mathématique puisse parfois être du ressort exclusif de l'ordinateur. Les maths ont longtemps été considérées comme le parangon de la science exacte par excellence, une science "publique", capable de produire des démonstrations dont les rouages abstraits sont aussi démontables que remontables à l'envi par quiconque en manifeste le désir auprès de n'importe quel "officier des archives mathématiques". Or, maintenant cette preuve mathématique sent l'odeur brûlée des calculateurs privés, des transistors qui chauffent, des fils de cuivre, des pannes intempestives de diodes luminescentes, jusqu'au sombre secret des boîtiers fermés de circuits électroniques...

Tu vois l'enjeu idéologique ?

Concernant les réseaux d'évacuation d'eau pluviale.
D'abord, il parait évident qu'il est important de trouver un compris pas trop bête entre l'efficacité, le prix, l'entretien, les évolution des constrictions etc.
Un tuyau peut évacuer une certaine quantité d'eau. Cette quantité est fonction de plusieurs facteurs particulièrement la section, la pente et la rugosité.
En un point donné, on sait (calcul préalable) la quantité d'eau à évacuer. On fait un choix fonction de l'expérience du concepteur. Etant donné la vitesse de l'eau dans les tuyaux, il y a un nouveau paramètre : la montée en charge qui se manifeste par le niveau de la ligne piézométrique.
On ne sait calculer un réseau d'évacuation que de l'amont vers l'aval, et on ne sait vérifier la qualité de ce réseau que de l'aval vers l'amont. donc on fait un premier calcul, puis on vérifie. Ce serait étonnant que ça marche du premier coup. Donc, on modifie certains choix, et on recommence.
Voilà le principe.
Si ce sujet t'intéresse, mon site explique cela : http://www.dlzlogic.com C'est le fenêtre de gauche.

Merci des infos sur cette vraie problématique d'ingénierie mécanique. Il est intéressant de noter que démontrer à l'aide d'un ordinateur des solutions optimales de ce problème physique (d'application hautement utile) ne crée pas autant de polémiques que des démonstrations comme le théorème des quatre couleurs (somme toute sans grand intérêt pratique). Encore une fois, ce n'est pas tant l'utilité attachée ou non à ces problèmes qui crée des frictions dans la communauté "scientifique", mais bien plutôt le degré d'exigence de "propreté" de la démonstration, bien plus élevé en mathématiques qu'en physique ou en sciences de l'ingénieur. Et là, avec le T4C, bang! Une démonstration "physique" d'un théorème de mathématique...