>> La démonstration a exigé l'usage d'un ordinateur
Et wikipédia rajoute que, plus récemment,
>> Il existe ainsi une version entièrement formalisée, formulée avec Coq par Georges Gonthier et Benjamin Werner, qui permet à un ordinateur de complètement vérifier le théorème des quatre couleurs.
Et là, ça a beau être un ordi, c'est bien de l'informatique (au sens « mathématique » du terme). Faut pas croire que c'est "j'appuie sur un bouton". C'est une vraie preuve, écrite à la main (sur un clavier), pas un programme qui cherche à ta place. L'avantage, c'est que si t'as une erreur dans ta preuve, ben, ça marche pas !
[^] # Re: La chèvre dans le champ rond
Posté par Axioplase ıɥs∀ (site web personnel) . En réponse au journal On ne sera jamais trop équitable.... Évalué à 2.
Et wikipédia rajoute que, plus récemment,
>> Il existe ainsi une version entièrement formalisée, formulée avec Coq par Georges Gonthier et Benjamin Werner, qui permet à un ordinateur de complètement vérifier le théorème des quatre couleurs.
Et là, ça a beau être un ordi, c'est bien de l'informatique (au sens « mathématique » du terme). Faut pas croire que c'est "j'appuie sur un bouton". C'est une vraie preuve, écrite à la main (sur un clavier), pas un programme qui cherche à ta place. L'avantage, c'est que si t'as une erreur dans ta preuve, ben, ça marche pas !