Démonstration et programmation

[Dlzlogic]

Bonjour,
On lit fréquemment des questions qui concernent le moyen de résoudre telle question avec l'informatique. Les plus courantes concernent naturellement l'utilisation d'Excel.
Là n'est pas mon propos.
Je veux parler de la notion de "démonstration". Un logiciel peut montrer par des calculs que la solution à telle équation, sous-entendu compliquée, peut être celle là. Pour mémoire, je pense au théorème des 4 couleurs, on sait le réaliser, mais à ma connaissance, on n'a pas démontré que ce théorème est vrai.
Donc, je crois que malgré la puissance considérable des ordinateurs et les capacités incontestables des informaticiens, il ne faut pas faire un amalgame entre une démonstration mathématique, opposable à n'importe qui, compte tenu des hypothèses de base et un programme informatique qui ne fait que faire des calculs suivant les règles précises et imposées par l'analyste et le programmeur.

[Sylviel]

ça tombe mal, le théorème des 4 couleurs est l'exemple typique de théorème démontré à l'aide de l'informatique.

http://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_quatre_couleurs

Ainsi il y a bien des cas où l'informatique vient en aide à la démonstration mathématique (et pas seulement à la mise en oeuvre des maths pour résoudre un problème).

[leon1789]

Un logiciel peut montrer par des calculs que la solution à telle équation, sous-entendu compliquée, peut être celle là.
(...)
il ne faut pas faire un amalgame entre une démonstration mathématique (...) et un programme informatique

Où a-t-on un exemple d'un tel amalgame ?

Un programme info et une preuve de maths sont deux choses différentes, l'un pouvant participer à l'autre, et réciproquement.

Par ailleurs, un programme informatique peut faire bien plus que résoudre des équations : calcul matricielle, calcul polynomial, calcul intégrale, ... et même faire des preuves de théorème de maths (cf Coq)

[Monsieur23]

Aloha,

Un programme info et une preuve de maths sont deux choses différentes

H. Curry et WA. Howard te disent bonjour !

[Sylviel]

Non, c'est là tout le problème de la preuve non constructive. Elle n'aboutit à rien.

Ben au théorème qu'elle montre quand même. Un résultat d'existence est intéressant en soit, quand bien même la preuve ne soit pas constructiviste.

[Monsieur23]

Ben au théorème qu'elle montre quand même. Un résultat d'existence est intéressant en soit, quand bien même la preuve ne soit pas constructiviste.

Oui, j'ai un peu exagéré avec "à rien". :lol3:
Mais une fois que tu sais que ton truc existe, ben tu ne peux pas en faire grand chose si tu n'as aucune idée de ce que c'est.

[Sylviel]

Je vais donner un exemple, pas forcément le plus convaincant, sur un domaine que je connais :
pouvoir montrer l'existence d'un point selle permet de garantir qu'un algorithme (numérique et implémentable) va converger. Dans le même genre l'existence d'une borne (quand bien même parfaitement incalculable) permet de montrer des résultats de convergence, d'effectuer des calculs (du type échange limite / intégrale) etc... Encore un autre exemple : l'existence d'un point dans l'intersection de deux ensemble montre qu'il n'est pas vide, et donc qu'il est vain de chercher à les séparer. En réfléchissant plus on doit pouvoir trouver tout plein d'exemple où la simple existence d'un objet à des conséquences pratique.

[Dlzlogic]

ça tombe mal, le théorème des 4 couleurs est l'exemple typique de théorème démontré à l'aide de l'informatique.

http://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_des_quatre_couleurs

Ainsi il y a bien des cas où l'informatique vient en aide à la démonstration mathématique (et pas seulement à la mise en oeuvre des maths pour résoudre un problème).

Bonjour Sylviel.
Il y a quelques temps, je ne suis intéressé à ce théorème, cette question était à la mode.
Je crois avoir à peu près tout lu à ce sujet l'époque. Il y avait entre autres les publications de quelqu'un qui était justement à l'origine de cette pseudo-démonstration à partir de l'informatique. Ce raisonnement m'intéressait.
J'ai essayé de le joindre, n'ayant pas de réponse, j'ai fini par appeler le secrétariat de l'X dont il se prétendait ancien élève. Il s'agissait en fait d'un fantôme.

En d'autres termes, c'est en parfaite connaissance de cause que j'ai choisi cet exemple.
Donc, je me répète, à ma connaissance, ce théorème n'est pas démontré, on a fait tourner des machines des centaines d'heures pour "vérifier" qu'il était crédibles, et la théorie de la démonstration par l'informatique est écrite par un auteur fantôme.

[Monsieur23]

Je vais donner un exemple, pas forcément le plus convaincant, sur un domaine que je connais :
pouvoir montrer l'existence d'un point selle permet de garantir qu'un algorithme (numérique et implémentable) va converger. Dans le même genre l'existence d'une borne (quand bien même parfaitement incalculable) permet de montrer des résultats de convergence, d'effectuer des calculs (du type échange limite / intégrale) etc... Encore un autre exemple : l'existence d'un point dans l'intersection de deux ensemble montre qu'il n'est pas vide, et donc qu'il est vain de chercher à les séparer. En réfléchissant plus on doit pouvoir trouver tout plein d'exemple où la simple existence d'un objet à des conséquences pratique.

Oui mais là, les théorèmes que tu cites sont de la forme
, dont tu donnes une preuve constructive (de ton x, tu construis une preuve de convergence).
Quand tu voudras montrer l'existence de ton x, tu feras souvent un raisonnement constructiviste (on ne demande pas en fait de construire explicitement l'objet pour être constructiviste, un algorithme permettant de l'approcher suffit ; par exemple, la limite d'une suite est connue dans le sens ou on peut la connaître avec une précision arbitraire).

[Dlzlogic]

J'allais dire ce que vient d'écrire Monsieur23, mais avec mes mots. Tu veux "démontrer" que c'est un point "selle", en fait tu veux effectuer le calcul qui permettra de le démontrer.
Par ailleurs tu as démontré que s'il y a un point selle, alors etc...
Donc l'informatique n'est qu'un outil qui peut servir, mais ce ne sera jamais qu'un outil. La démonstration mathématique, c'est autre-chose.

[Sylviel]

@Monsieur23 : non non dans l'exemple du point selle tu as besoin de l'existence d'un multiplicateur (obtenu par des théorèmes d'existence quelconque, pas forcément constructivise), pour assure la convergence de l'algorithme vers autre chose (la solution primale). Et il n'y a pas forcément de convergence vers le multiplicateur (dont on a pourtant besoin de l'existence).

@Dlzlogic : vu tes diverses affirmations erronnées récentes et plus anciennes tu comprendra que ton avis sur la question me paraît asser peu intéressant...

[Dlzlogic]

En réalité n'importe quel étudiant en mathématique, ou personne s'intéressant au domaine à entendu parler du théorème des 4 couleurs comme étant le premier théorème qui avait nécessité l'aide d'un ordinateur pour être démontré. L'ordinateur testant de manière systématique les milliers de cas qui prendrait des années à être prouvés à la main.

Ah, si c'est ce que tu appelles une preuve au sens mathématique, alors naturellement tu as raison.
Cette méthode montre simplement qu'on n'a pas trouve d'exemple contraire.
Le fantôme dont je parle évoquait le vrai sens de preuve Et si ce n'était pas un fantôme, pourquoi je n'aurais pas pu le retrouver.

[Sylviel]

Un exemple -trivial- de preuve mathématique qu'un ordinateur peut faire.

Montrer que tout les entiers naturels n plus petit que 10 sont tels que n² \leq 100

L'ordinateur prend chaque entier, l'élève au carré et le compare à 100. Tous les cas sont étudiés, donc la preuve est faite.

Une preuve avec l'aide d'un ordinateur fait cela sur des exemples bien plus complexe : l'ordinateur teste explicitement les milliers de cas qu'un humain pourrait faire à la main, mais cela demanderait très longtemps. Soyons précis : il n'y a pas forcément un nombre fini de cas à l'origine, le mathématicien le réduit à un nombre fini de cas, le plus petit possible, puis programme l'ordinateur pour tester les divers cas. Un exemple amusant existe autour du Rubik's cube.


Quant à ton histoire de fantome : je ne sais pas de qui tu parles puisque tu fais une affirmation dans le vide. Moi je t'ai donné des liens :
- vers wiki où tu as toute l'histoire de ce théorème
- vers un article de l'AMS
- vers un article de "combinatorial optimization", journal mathématique à comité de relecture
- vers le site de coq un projet inria dont l'objectif est de faire des preuves à l'aide de l'informatique. Mais puisque c'est "ridicule" je t'invite à contacter le directeur de l'INRIA pour lui dire que les divers chercheurs employés sur ce projet sont des planqués (bien qu'ils enseignent, publient etc) puisque cela n'a pas de sens.

Un jour il faudra que tu arrêtes de prendre le reste de la terre de haut en disant "je sais mieux que tout le monde, et puisque je suis si sûr de moi c'est que ça doit être vrai".

Désolé de m'énerver mais voir quelqu'un qui enchaine contre vérité sur contre vérité critiquer les travaux de mathématiciens sans références, sans arguments, et sans écouter les arguments que l'on peut lui renvoyer fini par me mettre hors de moi.

[fatal_error]

sans écouter les arguments que l'on peut lui renvoyer fini par me mettre hors de moi.

et c est l effet escompte.
Il vaut bien mieux ignorer ce genre de commentaires!

[leon1789]

Selon toi, à quoi servent les preuves essentiellement non constructives ?
(...)
Non, c'est là tout le problème de la preuve non constructive. Elle n'aboutit à rien.

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).

Je ne comprends pas de quoi tu veux des exemples ?

Je pensais que s'il était nécessaire, on pourrait donner des exemples de preuves de maths classiques non constructives, et des exemples d'algos qui ne prouvent rien. Mais je constate qu'on se comprend sans exemple. (...et qu'entre temps, des exemples ont été évoqués).

[Dlzlogic]

Juste une petite précision que j'ai oubliée, le fantôme dont je parle a fait son apparition APRES cet article de l'AMS, et prétendait justement apporter une VRAIE démonstration à l'aide de l'informatique.
Ton exemple avec les nombres entiers est une vérification. 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" tout simplement parce que personne ne le conteste, c'est évident pour tout le monde, par exemple, sur une année, la durée du jour est égale à celle de la nuit. Ca c'est "vrai". 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.
Si tu as des commentaires personnels, les MP sont faits pour ça.

[adrien69]

En réalité n'importe quel étudiant en mathématique, ou personne s'intéressant au domaine à entendu parler du théorème des 4 couleurs comme étant le premier théorème qui avait nécessité l'aide d'un ordinateur pour être démontré. L'ordinateur testant de manière systématique les milliers de cas qui prendrait des années à être prouvés à la main.

En fait non :/
Désolé...

[Sylviel]

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 ?

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.

Dans l'exemple du Rubiks cube il y avait à l'origine 43’252’003’274’489’856’000 positions à tester,
au final l'ordinateur en a testé 55’882’296. Soit beaucoup trop pour être testé par un humain, mais beaucoup moins que si on avait été brutal (ce qui aurait aussi été une preuve). Le résultat montré est (en langage français) :
"Pour résoudre le rubik's cube il faut au maximum 20 coups" (et on a des exemples nécessitant 20 coups.

Un article en français dessus : http://www.theologeek.ch/2013/10/08/nombre-dieu-20/

[Sylviel]

@Adrien : je t'invite à te renseigner alors ;-) ça fait partie de la culture mathématique au même titre que le théorème de Fermat :zen:

[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.