Sauf qu’aujourd’hui certaines preuves utilisent des ordis pour faire des bouts de démonstration. Ça complique les choses d’une part parce que si tu veux enlever l’algo de l’équation ça produit des preuves dont la taille est sans commune mesure avec les preuves d’avant. Donc un truc probablement fastidieux et long à vérifier à la main, on a ptete mieux à faire du temps et des nerfs de nos meilleurs matheux. Ou alors ça nécessite de se convaincre que le programme utilisé est effectivement capable de produire une démonstration de ce qu’il est supposé montrer. Donc qu’il est sans bug. Les matheux tradis détestent ces démonstrations d’ailleurs, parce que les ordis servent souvent à faire une exploration systématique d’un certain nombre de cas qui peuvent exploser combinatoirement, et qu’ils préfèreraient un argument qui règle tout de manière plus synthétique avec une belle théorie. Et que ça rend difficile de se convaincre de la correction de la preuve. Mais rien ne dit que ça existe dans l’absolu et que toutes les preuves sont « courtes ». Au contraire est certains qu’il y a des objets comme des indécidables ou des propositions à démonstrations très très longue dans un système logique donné. cf. https://fr.wikipedia.org/wiki/Longueur_d%27une_d%C3%A9monstration
Par exemple pour P=?NP ou des « preuves » sont produites régulièrement par tout un chacun et envoyés à des experts, il y a de bonne chances pour que personne ne lise jamais la proposition, trop long et peu probable que ce soit correct de la part d’un non expert du domaine. Si ça se trouve elle a été trouvée mais personne n’a ouvert le mail et elle a zéro chances d’être publiée :) Si le type fournit une preuve prouvée (inception) il a peut être plus de chances d’être pris au sérieux.
[^] # Re: Math
Posté par thoasm . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 4.
Sauf qu’aujourd’hui certaines preuves utilisent des ordis pour faire des bouts de démonstration. Ça complique les choses d’une part parce que si tu veux enlever l’algo de l’équation ça produit des preuves dont la taille est sans commune mesure avec les preuves d’avant. Donc un truc probablement fastidieux et long à vérifier à la main, on a ptete mieux à faire du temps et des nerfs de nos meilleurs matheux. Ou alors ça nécessite de se convaincre que le programme utilisé est effectivement capable de produire une démonstration de ce qu’il est supposé montrer. Donc qu’il est sans bug. Les matheux tradis détestent ces démonstrations d’ailleurs, parce que les ordis servent souvent à faire une exploration systématique d’un certain nombre de cas qui peuvent exploser combinatoirement, et qu’ils préfèreraient un argument qui règle tout de manière plus synthétique avec une belle théorie. Et que ça rend difficile de se convaincre de la correction de la preuve. Mais rien ne dit que ça existe dans l’absolu et que toutes les preuves sont « courtes ». Au contraire est certains qu’il y a des objets comme des indécidables ou des propositions à démonstrations très très longue dans un système logique donné. cf. https://fr.wikipedia.org/wiki/Longueur_d%27une_d%C3%A9monstration
Par exemple pour P=?NP ou des « preuves » sont produites régulièrement par tout un chacun et envoyés à des experts, il y a de bonne chances pour que personne ne lise jamais la proposition, trop long et peu probable que ce soit correct de la part d’un non expert du domaine. Si ça se trouve elle a été trouvée mais personne n’a ouvert le mail et elle a zéro chances d’être publiée :) Si le type fournit une preuve prouvée (inception) il a peut être plus de chances d’être pris au sérieux.