Pour ce qui est du théorème des quatre couleurs, quelques précisions.
C'est le théorème qui dit que si les tous les pays étaient d'un seul tenant (pas comme les USA avec l'alaska), alors on pourrait toujours colorier une carte avec seulement 4 couleurs.
D'une part, le résultat de Gonthier et Werner est de 2004 et pas de 2002.
De plus, c'est une réécriture dans le système COQ de la démonstration de Robertson, Sanders, Seymour et Thomas de 1996. La preuve des 4 fous est une simplification de la preuve de Appel et Haken. Elle part du principe que si il existe un graphe planaire seulement 5 coloriable, alors il est existe un le plus petit possible. Avec des arguments bien forts, ils se ramènent à un nombre finis de cas. Le problème est que le nombre fini de cas reste trop gros pour être traité à la main. La fin de la démonstration utilise donc un ordinateur pour traiter les cas de base. Le problème est que les ordinateurs, c'est buggé. Donc la preuve...
L'intérêt du travail de Gonthier et Werner est que COQ est un système de démonstration assistée. En gros, avec COQ, on est sûr de ne pas oublier de cas tordu. Mais COQ est aussi un programme. Il peut donc être lui aussi buggé. C'est vrai sauf que COQ permet de produire un certificat dont il est très simple de vérifier qu'il est juste (ou pas). Cette partie du programme a même pu être prouvée à la main. On peut donc très raisonnablement penser que la preuve est juste.
[^] # Re: Ha ha ha
Posté par fmaz fmaz . En réponse à la dépêche Disparition de M. Gilles KAHN, Président de l'INRIA, membre de l'Académie des Sciences. Évalué à 5.
C'est le théorème qui dit que si les tous les pays étaient d'un seul tenant (pas comme les USA avec l'alaska), alors on pourrait toujours colorier une carte avec seulement 4 couleurs.
D'une part, le résultat de Gonthier et Werner est de 2004 et pas de 2002.
De plus, c'est une réécriture dans le système COQ de la démonstration de Robertson, Sanders, Seymour et Thomas de 1996. La preuve des 4 fous est une simplification de la preuve de Appel et Haken. Elle part du principe que si il existe un graphe planaire seulement 5 coloriable, alors il est existe un le plus petit possible. Avec des arguments bien forts, ils se ramènent à un nombre finis de cas. Le problème est que le nombre fini de cas reste trop gros pour être traité à la main. La fin de la démonstration utilise donc un ordinateur pour traiter les cas de base. Le problème est que les ordinateurs, c'est buggé. Donc la preuve...
L'intérêt du travail de Gonthier et Werner est que COQ est un système de démonstration assistée. En gros, avec COQ, on est sûr de ne pas oublier de cas tordu. Mais COQ est aussi un programme. Il peut donc être lui aussi buggé. C'est vrai sauf que COQ permet de produire un certificat dont il est très simple de vérifier qu'il est juste (ou pas). Cette partie du programme a même pu être prouvée à la main. On peut donc très raisonnablement penser que la preuve est juste.