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 ?
Réponses
-
Il y a plusieurs cas célèbres où les preuves controversées sont trop longues et trop difficiles pour être vérifiées par les "experts" du domaine, qui n'ont pas forcément le temps de se consacrer à de la vérification. Je pense notamment à un mathématicien japonais qui prétend avoir démontré la conjecture $abc$ depuis des années, mais personne n'a pu vérifier l'intégralité de sa preuve car celui-ci a développé toute une théorie qu'il est le seul à connaître véritablement.
-
Je connais ce cas Poirot, mais à nouveau comment accepter une preuve si le lecteur, même expert, est incapable de la suivre ?
-
Oui, c'est toujours le problème de la différence entre la théorie et la pratique: en théorie, il n'y a pas de différence, mais en pratique, si. En théorie toute preuve peut s'exprimer comme un objet syntaxique qu'il est parfaitement trivial de vérifier mécaniquement (même pas besoin d'experts du domaines: un algo suffit). En pratique personne n'a envie de perdre son temps à dérouler une preuve à un niveau de détail où toutes les trivialités doivent être démontrées, alors je n'imagine même pas ce que deviennent les "on identifie" ou autre. Récemment, si mes souvenirs sont bon, quelqu'un a formalisé en COQ une preuve du théorème central limite et c'était un achievement (désolé je ne suis vraiment pas fond of des anglicismes, mais je n'arrive pas à trouver le mot français qui convient).
-
Pour moi les "on identifie" sont effectivement durs à développer proprement en entier, mais si le point qui fait débat se situe là alors il faut bien le faire. Si c'est dur à écrire c'est justement qu'il y a peut-être une non trivialité quelque part.
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. -
Je ne dis pas du tout qu'en l'occurence c'est un "on identifie" qui pose problème: je n'en sait rien du tout. C'était juste pour faire prendre la mesure de la différence entre la preuve compréhensible pour nous et la preuve objet-syntaxique-formel.
-
Si ça se trouve (encore une fois j'en sais rien, viens, donne-moi la main) pour clarifier "le point qui fait débat" il faut en passer par formaliser l'ensemble de la preuve.
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... -
Pas comprendre bien les autres langues non maternelles.
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 -
En gros le lien dit qu'en théorie un papier devrait être sans faille, et vérifiable. Mais ça c'est la théorie comme dit Shash d'Ock En pratique il y a souvent des théorèmes qui ont des failles ou qui sont faux Mais généralement les problèmes sont mineurs et vites identifiés et corrigés, au moins pour les théorèmes importants.
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. -
Un autre exemple de bataille entre spécialistes ici : A preprint of Sela concerning the work of Kharlampovich-Miyasnikov.
-
Exploit est trop fort. Accomplissement me va. Merci.
-
Christophe faisais semblant (je pense) de confondre démonstration mathématique et preuve formelle. Ton fil amène en fait plusieurs questions : qu'est-ce qu'une preuve mathématique et quand peut-on dire qu'un théorème a été démontré ?
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. -
@skyffer3
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. -
Mojojo j'aime beaucoup ta citation. Mais ça ne contredit pas qu'en théorie on devrait pouvoir dérouler la démonstration jusqu'à en faire une preuve... Sinon ça veut dire qu'on ne sait pas pourquoi on est convaincu.
-
Merci à tous. La définition donnée par mojojojo est très pertinente, mais comme le suggère Shah d'Ock, si même des experts sont pas convaincus c'est qu'il faut dérouler plus. En tout cas si la taille des preuves continent d'augmenter ça risque de poser problème à long terme. Mais j'imagine qu'un effort considérable est aussi mis dans l'élaboration de nouvelles théories qui ont pour but de donner un cadre simplificateur.
-
Le problème c'est que pour tout $N$ il n'y a qu'un nombre fini d'énoncés mathématiques (respectivement de preuves) de moins de $N$ caractères. Évidemment on peut introduire de nouvelles abréviations pour simplifier les notations, de nouveaux théorèmes pour simplifier les preuves, mais ce qu'on gagne de ce côté on le perd inévitablement du côté de la masse de chose à commencer par apprendre.
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.2K Toutes les catégories
- 9 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 65 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 314 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 773 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 40
+23 Invités