Démonstration et programmation

[leon1789]

Si tu as des commentaires personnels, les MP sont faits pour ça.

A ce sujet, faut voir le contenu de certains MP de ta part :

C'est marrant, avant, tes réaction m'énervait, il est assez rare que je n'arrive pas à me faire comprendre, maintenant, je sais, ça ne fait plus de doute, tu n'es qu'un nuisible sans aucun intérêt. A vomir.

On comprendra que je ne désire plus recevoir tes fameux MP...

Il y a, me semble-t-il, une différence entre "démontrer une proposition" et "dire, avec vérification, qu'une chose est vraie"

Pour le coup, je ne vois aucune différence entre une preuve et une vérification exhaustive : un raisonnement abstrait n'est pas plus une preuve qu'une vérification calculatoire ! Exemple : pour démontrer que, pour tout entier n, l'entier n.(n^2-1) est multiple de 6, tu peux factoriser n(n-1)(n+1) et utiliser ppcm(2,3) =6 (là, on le fait sans ordi), ou bien travailler dans Z/6Z est vérifier "à la main" que n.(n^2-1) = 0 pour les 6 classes (on peut utiliser un ordi pour cela). Ce sont bien deux preuves !

Certes, on peut aimer ou pas certaines preuves (les maths ont effectivement un goût), mais cela n'empêche pas que ce sont toutes des preuves...

par exemple, sur une année, la durée du jour est égale à celle de la nuit. Ca c'est "vrai".

Dit comme cela, pour moi c'est de la "croyance".

La démonstration, c'est une autre paire de manche, il faudrait d'abord définir ce qu'est une année, définir le plan de l'écliptique, le temps de rotation de la terre etc. Et, en fait, je crois que ce n'est pas tout à fait vrai, mais il s'agit de lointains souvenirs.

Donc on peut croire quelque chose qui n'est pas vrai, on est d'accord.

[leon1789]

Si tu as des commentaires personnels, les MP sont faits pour ça.

A ce sujet, faut voir le contenu de certains MP de ta part :

Dons j'hésite entre 2 qualificatifs à te donner, soit "rigolo" soit "nuisible". Etant donné ce qui a été investi pour tes études, je pencherais plus pour le second.
(...)
C'est marrant, avant, tes réaction m'énervait, il est assez rare que je n'arrive pas à me faire comprendre, maintenant, je sais, ça ne fait plus de doute, tu n'es qu'un nuisible sans aucun intérêt. A vomir.

On comprendra que je ne désire plus recevoir tes fameux MP...

Il y a, me semble-t-il, une différence entre "démontrer une proposition" et "dire, avec vérification, qu'une chose est vraie"

Pour le coup, je ne vois aucune différence entre une preuve et une vérification exhaustive : un raisonnement abstrait n'est pas plus une preuve qu'une vérification calculatoire ! Exemple : pour démontrer que, pour tout entier n, l'entier n.(n^2-1) est multiple de 6, tu peux factoriser n(n-1)(n+1) et utiliser ppcm(2,3) =6 (là, on le fait sans ordi), ou bien travailler dans Z/6Z est vérifier "à la main" que n.(n^2-1) = 0 pour les 6 classes (on peut utiliser un ordi pour cela). Ce sont bien deux preuves !

Certes, on peut aimer ou pas certaines preuves (les maths ont effectivement un goût), mais cela n'empêche pas que ce sont toutes des preuves...

par exemple, sur une année, la durée du jour est égale à celle de la nuit. Ca c'est "vrai".

Dit comme cela, pour moi c'est de la "croyance".

La démonstration, c'est une autre paire de manche, il faudrait d'abord définir ce qu'est une année, définir le plan de l'écliptique, le temps de rotation de la terre etc. Et, en fait, je crois que ce n'est pas tout à fait vrai, mais il s'agit de lointains souvenirs.

Donc on peut croire quelque chose qui n'est pas vrai, on est d'accord.

[Monsieur23]

Disons que, même si elle n'aboutit à rien algorithmiquement parlant, elle a le mérite de commencer un travail, de "déblayer le terrain" comme on dit. Il conviendrait ensuite de réaliser un travail plus précis (=> maths constructives).

On est d'accord, je ne crache pas non plus sur les preuves non constructives, il y en a de très belles
Mais ce n'est pas vraiment ma vision des maths.

Non une démonstration c'est utiliser des résultats que l'on sait vrai pour joindre les hypothèses d'un théorème au résultat. Enfin c'est ce que les mathématiciens appellent une démonstration depuis 2500 ans... D'après toi c'est quoi la définition d'une démonstration ?

En fait, une démonstration, c'est formellement un arbre de preuve dans le système de ton choix (souvent en maths usuelles, le système à la Hilbert, et en logique/info on utilise plutôt la déduction naturelle ou le calcul des séquents).

Au cours d'une démonstration il peut y avoir disjonction de cas et études de ces différents cas. Quand il y en a un nombre réduit c'est faisable à la main, quand il y en a un nombre important l'ordinateur peut s'avérer utile.

La vraie question à se poser, c'est à quel point on peut faire "confiance" à l'ordinateur ?
Finalement, un bout de ta démonstration se trouve dans une "boîte noire" qu'il est (souvent) difficile d'ouvrir.

[Doraki]

La vraie question à se poser, c'est à quel point on peut faire "confiance" à l'ordinateur ?
Finalement, un bout de ta démonstration se trouve dans une "boîte noire" qu'il est (souvent) difficile d'ouvrir.

Et à quel point peut-on faire confiance à un être humain ? vu le nombre de typos et d'erreurs de toutes sortes qu'il y a dans les bouquins et les articles, je fais vachement plus confiance à Coq qu'à n'importe qui.

[Monsieur23]

Et à quel point peut-on faire confiance à un être humain ? vu le nombre de typos et d'erreurs de toutes sortes qu'il y a dans les bouquins et les articles, je fais vachement plus confiance à Coq qu'à n'importe qui.

Disons qu'il est plus facile de demander à un humain d'expliciter son raisonnement qu'à Coq.

[Dlzlogic]

Bonjour,
Pardon pour cette question : qui est Coq ?

[leon1789]

Et à quel point peut-on faire confiance à un être humain ? vu le nombre de typos et d'erreurs de toutes sortes qu'il y a dans les bouquins et les articles, je fais vachement plus confiance à Coq qu'à n'importe qui.

Effectivement, errare humanum est.

En plus, dans un certain sens, accepter une preuve est un acte subjectif : nous avons tous été dubitatif devant une preuve de quelqu'un qui affirmait correcte et suffisante. Et vise versa...

Cela dit, on peut relire et corriger un exposé à la dimension humaine, c'est plus difficile de le faire sur un gros calcul via ordinateur (à moins d'utiliser aussi un ordi, bis repetita). Même Coq a été bugué (il y a quelques années). Ok, le bug a été détecté, identifié et corrigé. Mais à quand le prochain bug ?

[leon1789]

Bonjour,
Pardon pour cette question : qui est Coq ?

Faut apprendre à lire :

L'utilisation d'assistants de preuves (comme Coq) ...

Et coq c'est ça : http://coq.inria.fr/

[Sylviel]

http://coq.inria.fr/what-is-coq

Pour résumer : des équipes de chercheurs de l'INRIA. Le langage de programmation derrière c'est OCaml & C.

[Dlzlogic]

Pour être tout à fait complet, on pourrait imaginer que le schéma suivant a été mis au point.
Soit A un ensemble limité de propositions. Toutes ces proposition sont la conclusion d'une démonstration connue, par exemple que le centre du cercle circonscrit à un triangle est le point de concours des médiatrices.
Soit un module M capable de vérifier que telle proposition que l'on cherche à démontrer entre dans le cadre de l'ensemble A. Par "vérifier" je veux dire assurer qu'il est impossible que la conclusion ne soit pas bonne, et non pas simplement constater qu'on n'a pas trouvé de contre-exemple.

Petit exemple simple : soit un certain théorème qui serait démontré si on démontre que les droites D1 et D2, résultant des différentes étapes du calcul et/ou de la démonstration, sont parallèles. Etant donné le nombre fini de chiffres significatifs des valeurs calculées par un ordinateur, il est impossible de conclure. Par contre, on peut conclure que c'est vrai, compte tenu d'une certaine tolérance.

Lorsque j'ai lu l'article sur les 4 couleurs dont j'ai parlé au début, j'imaginais que cette question [module M] avait été résolue, d'où mon intérêt pour la question.

On pourrait imaginer le schéma suivant dans le cadre des 4 couleurs.
1- on détermine de façon exhaustive toutes les dispositions possibles de zones accolées,
2- on démontre que plusieurs de ces schémas du [1-] accolés ne produisent pas de disposition non prévue dans la liste des dispositions.
3- la machine peut alors permettre de vérifier que les points 1 et 2 sont des éléments de démonstration.
Même comme cela, je ne suis pas sûr que cette vérification ait valeur de démonstration. Et à mon avis on ne peut pas démontrer les points 1 et 2.

Pour rester dans ce même cadre des 4 couleurs.
Il est intéressant de pouvoir colorier un ensemble de zones, par exemple les départements français, avec seulement 4 couleurs. On suppose naturellement que c'est possible, là n'est plus la question, mais comment le faire ? C'est un peu hors sujet, mais tant-pis.

[Sylviel]

Si tu n'es pas sûr que cela ai valeur de démonstration je t'invite à écrire à l'AMS, ainsi que les autres journaux qui ont publié la preuve du théorème des 4 couleurs...

[Sylviel]

Petit exemple simple : soit un certain théorème qui serait démontré si on démontre que les droites D1 et D2, résultant des différentes étapes du calcul et/ou de la démonstration, sont parallèles. Etant donné le nombre fini de chiffres significatifs des valeurs calculées par un ordinateur, il est impossible de conclure. Par contre, on peut conclure que c'est vrai, compte tenu d'une certaine tolérance.

Ce n'est absolument pas comme ceci que fonctionne un programme de preuve.

Grossièrement l'idée correspond à ta seconde proposition :

-> On rentre des axiomes (dont des règles de logiques)
-> En utilisant exclusivement ces axiomes ont construit des propositions
-> En utilisant les propositions ont construits d'autres propositions etc...

Il n'y a pas de "calcul numérique avec imprécision" mais uniquement vérification que les divers éléments s'enchaîne bien et que l'on n'a pas utilisé de "règle factice".


Pour le théorème des 4 couleurs c'est bien l'idée (comme expliqué plusieurs fois déjà) :
- les matheux réduisent l'ensemble des possibilités à un nombre fini de cas
- construisent des méthodes pour vérifier chacun de ces cas
- demande à l'ordi d'utiliser les méthodes données sur les milliers de cas à tester

Le rubiks cube (lien en français donné plus haut) explique très bien la démarche.

Si après tout cela tu es convaincu qu'il ne s'agit pas d'une preuve je t'invite à écrire à l'AMS pour leur dire qu'ils ont publié un article faux (ainsi qu'aux autres journaux)...