Statut d'une preuve
Certains ont affirmé ici même qu'une preuve, même d'un théorème professionnel moderne, est vérifiable par un enfant de maternelle (si on lui donne un temps non limité), affirmation que j'avais contestée à l'époque.
Mais quand je vois cela je suis choqué : https://mathoverflow.net/questions/282742/endless-controversy
Il existe donc des preuves, où l'ordinateur n'intervient pas, mais dont le statut est contesté entre experts sur plusieurs années voire décennies ??? Je ne comprends pas, si un point fait débat, que ceux qui défendent la preuve développent l'argument jusqu'à retomber sur un point d'accord, sinon c'est qu'il reste du flou.
Je suis parfaitement conscient que développer tous les micro détails d'une preuve peut multiplier sa taille, mais ça me paraît indispensable si même des experts contestent son statut. Ça peut être long, mais si c'est trop compliqué à faire c'est qu'il y a un loup quelque part, non ?
Est-ce que des pros ont un avis sur ce sujet ?
Mais quand je vois cela je suis choqué : https://mathoverflow.net/questions/282742/endless-controversy
Il existe donc des preuves, où l'ordinateur n'intervient pas, mais dont le statut est contesté entre experts sur plusieurs années voire décennies ??? Je ne comprends pas, si un point fait débat, que ceux qui défendent la preuve développent l'argument jusqu'à retomber sur un point d'accord, sinon c'est qu'il reste du flou.
Je suis parfaitement conscient que développer tous les micro détails d'une preuve peut multiplier sa taille, mais ça me paraît indispensable si même des experts contestent son statut. Ça peut être long, mais si c'est trop compliqué à faire c'est qu'il y a un loup quelque part, non ?
Est-ce que des pros ont un avis sur ce sujet ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
D'autant plus qu'on ne demande pas de retaper toute la preuve en coq, juste de développer le point qui fait débat.
Et si ça se trouve aussi chaque parti est si bien persuadé d'avoir raison qu'il se dit que ça ne va pas être long de convaincre l'autre, alors plutôt que de s'attaquer à un boulot rébarbatif mais infaillible, on passe par des expédients en espérant régler le problème rapidement. Et ça fait dix ans que ça dure...
Peux-tu résumer ce qui est dit en lien en jurant que c'est fidèle mais pas Castro, s'il te plaît skyffer ?
S
Sauf que parfois, les détails techniques sont tels qu'une preuve, même importante dans le domaine, peut être contestée par d'autres experts pendant des années voire des décennies.
Lors d'une présentation du logiciel COQ l'orateur nous avais proposé sa définition de démonstration mathématique, que j'aime bien :
"une démonstration mathématique est un texte, un dessin, un programme... fait pour convaincre un mathématicien qu'il existe une preuve formelle du résultat" (citation non exacte, c'était il y a plusieurs années déjà).
Le mathématicien en question peut être un ami, collègue, correcteur d'un examen, soi même, le lecteurs de son livre... et la preuve changera en conséquence. D'ailleurs avec cette définition une preuve formelle, à moins d'être implémentée dans COQ, n'est quasiment jamais une démonstration mathématique. Evidemment avec cette définition une démonstration mathématique est tout sauf un objet mathématique, ce n'est donc pas si étonnant que dans certains cas extrêmes les mathématiciens n'arrivent pas à s'entendre sur le statu d'une preuve.
Un autre exemple de démonstration faisant débat : classification des groupes simples finis. Citation de la page wikipédia : "un ensemble de travaux, principalement publiés entre environ 1955 et 1983, qui a pour but de classer tous les groupes finis simples. En tout, cet ensemble comprend des dizaines de milliers de pages publiées dans 500 articles par plus de 100 auteurs." sans oublier les parties non publiées de la preuve. On comprend pourquoi certains sont sceptique quant à la véracité de la preuve et pourquoi personne ne s'amuse à relire la preuve en entier.
@shah d'ock : Sur la page wikipédia de COQ on peut voir que les démonstration du théorème des 4 couleurs et du théorème de Feit Thompson ont été vérifiées par COQ. Donc il y a plus impressionnant que le TCL mais si mes souvenirs sont bon cela à demandé le travail de plusieurs personnes pendant plusieurs années pour écrire ces preuves vérifiables par COQ.
Je pointe un papier (certes technique) d'un historien https://www.emis.de/journals/SC/1998/3/pdf/smf_sem-cong_3_243-273.pdf
Ce que tout le monde peut comprendre : le sous-titre ``A Comedy of Errors'' à propos du douzième problème d'Hilbert. Et comment l'autorité d'Hilbert va empêcher, pendant des années, la découverte d'une erreur dans une conjecture incorrecte d'Hilbert. Cf le résumé en français par exemple.