Je veux bien croire que la première preuve de 1976 était peu fiable, vu qu'elle était écrite dans un langage qui ne garantissait en rien la correction du résultat (me semble que c'était du C, mais je ne suis pas sûr). Mais dire que la preuve moderne en Coq est sale[1], c'est transférer la saleté du problème vers la preuve.
La démonstration du théorème des quatre couleurs est fondamentalement technique au vu de la quantité de sous-cas à explorer. Beaucoup de problèmes de graphes sont dans cette situation, ce qui fait que la preuve ne peut pas être facilement appréhendée par un être humain. Et ça n'est pas pour plaire aux matheux, qui n'arrêtent pas de grogner contre la preuve assistée par ordinateur sous des prétextes philosophiques.
[1] Par contre, le code de Coq est plutôt sale, lui.
[^] # Re: En souvenir de son infirmation de la conjecture des quatre couleurs.
Posté par Perthmâd . En réponse au journal Martin Gardner (1914-2010). Évalué à 1.
La démonstration du théorème des quatre couleurs est fondamentalement technique au vu de la quantité de sous-cas à explorer. Beaucoup de problèmes de graphes sont dans cette situation, ce qui fait que la preuve ne peut pas être facilement appréhendée par un être humain. Et ça n'est pas pour plaire aux matheux, qui n'arrêtent pas de grogner contre la preuve assistée par ordinateur sous des prétextes philosophiques.
[1] Par contre, le code de Coq est plutôt sale, lui.