Démonstration automatique de théorèmes
Bonjour,
En lisant wiki
https://fr.wikipedia.org/wiki/Démonstration_automatique_de_théorèmes et avec l'avancé de l'informatique et les mathématiques, je me demande si un jour, il sera possible d'avoir un logiciel qui permet de démontrer des théorèmes ( et non pas seulement de les vérifier ). Est- ce que cela est possible theoriquement ?
Merci
En lisant wiki
https://fr.wikipedia.org/wiki/Démonstration_automatique_de_théorèmes et avec l'avancé de l'informatique et les mathématiques, je me demande si un jour, il sera possible d'avoir un logiciel qui permet de démontrer des théorèmes ( et non pas seulement de les vérifier ). Est- ce que cela est possible theoriquement ?
Merci
Le 😄 Farceur
Réponses
-
L'article dit pourtant que "Les démonstrateurs automatiques de théorème ont résolu des conjectures intéressantes difficiles à établir".
C'est seulement dans la section suivante, "Problèmes liés", qu'il parle de la vérification de preuves humaines. -
gebrane0 a écrit:Est- ce que cela est possible theoriquement ?
Oui et c'est très simple à démontrer : tu prends un singe qui tape sur une machine aléatoirement et envoie des bouts de texte aléatoirement. Tu le laisse produire pleins de bouts de texte (laisse lui plein de temps hein).
À l'autre bout, tu mets ton vérifieur qui lit les textes : si c'est une preuve valide, il accepte. Sinon, il jette. Au bout d'un moment, tu auras une preuve de ton théorème (et l'intégralité des Bourbaki aussi).
Bien sûr en pratique, 99.999999% des textes produits par le singe ne seront même pas corrects syntaxiquement parlant, mais tu as demandé "théoriquement".
Si la version probabiliste ne te plaît pas, tu peux utiliser un version déterministe : au lieu du singe, tu prends une machine qui énumère un à un tous les textes possibles (c'est dénombrable donc énumérable). -
Oui: sans plus de précision sur "prouver des théorèmes" tu peux écrire le programme suivant:
Let prouve_infinité () =
print_string "Supposons qu'il y ait un ensemble fini de nombres premiers. Considérons leur produit plus un. C'est un entier qui n'est divisible par aucun nombre premier. Contradiction."
;;
Plus sèrieusement (mais pas trop quand même): tu peux aussi écrire un programme qui simule l'Univers. Alors en particulier si tu attends assez longtemps il va simuler des mathématiciens, qui vont prouver des théorèmes...
Par contre ce qu'on sait qu'il est impossible de faire, c'est un programme qui prend un énoncé d'arithmétique et qui te dit si c'est un théorème d'arithmétique (à moins que l'arithmétique ne soit contradictoire auquel cas tout énoncé est un théorème). -
"tu peux aussi écrire un programme qui simule l'Univers"
Ce "peux" ne serait-il pas un peu trop optimiste ? -
Si la question porte sur la possibilité de démontrer des théorèmes et non tous les théorèmes, alors remarque que, en général, les vérificateurs de preuve peuvent aussi déjà prouver des théorèmes. En général, ils ne demandent pas à ce qu'on écrive la preuve formelle en entier, car ils sont capables de prouver automatiquement certains théorèmes "triviaux" et donc de compléter la preuve donnée par l'utilisateur. Evidemment, ces théorèmes "triviaux" ne sont pas des théorèmes non encore prouvés par des humains (c'est peut-être cette sorte de théorèmes que tu avais en tête?).
-
Pour ce qui est du singe qui tape du texte et l'équivalent moderne de ce cliché : https://fr.scribd.com/doc/14161596/Mathematiques-experimentales
-
Dans l'article cité en lien je suis tombé sur "d'hors et déjà". On écrit "d'ores et déjà".
-
Merci Shah d'Ock, c'est connu comme le houblon, et il faut d'orge et d'orgeat en prendre note.
-
Je m'interroge aussi sur l'utilisation des anglicismes "digits" et "super-computer".
-
Il y a tout de même une grosse différence entre les approches évoquées par sebsheep et l'article de JJ: en effet, dans les deux cas un texte aléatoire est produit, mais pour une démonstration, il existe un algorithme trivial pour vérifier qu'elle est correcte. A l'inverse, l'inverseur de Plouffe ne donne que des conjectures, dont il n'est pas trivial de vérifier si elles sont vraies (et elles sont parfois fausses...)
-
D'ores en avant JJ sera bien inspiré de consulter Shah d'Ock avant de publier !
-
Juste une petite rectification :J ai dit "denombrable donc enumerable" mais ce sens la est faux (l ensemble des programmes qui s arrêtent est denombrable non enumerable). Par contre l ensemble des textes est bien enumerable, un alphabet fini étant fixé.
-
Oui, et l'ensemble des preuves est également énumérable.
-
Bonsoir à tous,
Il est surprenant que tant de commentaires aient été postés au sujet d'un papier datant de presque dix ans et qui plus est n'a pas été publié, seulement mis sur internet (Qui plus est, papier impubliable ! ). J'espère quand même que la pièce maîtresse de l'article (l'illustration) vous a réjoui.
A la prochaine occasion, j'en ai encore sous le coude quelques autres qui ne valent guère mieux.
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
- 69 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
Qui est en ligne 20
+15 Invités