Discussion:Démonstration automatique de théorèmes

La traduction d'une partie de l'article et une question?

Bonjour je voulais poser une question sur wikipedia, et j'en ai profité pour traduire une partie de l'article, ce travail de traduction nécessite une vérification je pense.

Et puis je suis conscient que ce n'est pas l'endroit pour parler de cela (wikipedia), mais je voulais vous proposer une idées qui probablement existe déjà:

Je me dis qu'un bon moyen d'établir un logiciel qui répond aux questions des problèmes mathématiques (ce que n'est pas un démonstrateur automatique de preuve, puisque un démonstrateur automatique de preuve vérifie un théorème et ne répond pas à n'importe quel type de question mathématique), est justement de répondre à des question intermédiaire:

_ par exemple: trouver un théorème vérifiant certaines caractéristiques, par exemple pour la tour de hanoi, la question serait " trouver une séquence permettant d'arriver au but", on pourrait répondre à cette question dans un théorème vérifiant certaines caractéristiques, et les étapes intermédaires seraient des théorèmes intermédiaires vérifiant certaines caractéristiques.

_ J'y ai pas mal réfléchis et je me suis rendu compte que tout les problèmes compliqués se résolvent ainsi (du moins avec l'astuce que je viens de décrire) par exemple laser reflection ou autres..

--Nicobzz (d) 12 février 2012 à 23:07 (CET)

Je crains que l'on soit bloqué par le fait qu'on ne sait pas si P=NP. Je pense que comme P=/=NP, les problèmes compliqués resteront compliqués et le problème de trouver des démonstrations restera difficile. --Pierre de Lyon (d) 17 février 2012 à 15:49 (CET)

Merci Pierre de m'avoir répondu. La logique mathématique ne fait pas parti de mes études de base donc je risque de dire des bétises, vous ne m'en voudrez pas je pense: Je ne sais pas ce que signifie P et NP (enfin je comprend que c'est en rapport avec la complexité des problèmes et donc le temps d'éxecution d'un programme pour le résoudre), il faudrait que je me renseigne mieux à propos de ces notions.

Mais voila mon point de vue: Je pense que l'ordinateur ne fera surement jamais mieux que l'être humain, mais il doit pouvoir l'égaler à un coefficient prés: Grosso modo, si un humain met environ 1 mintues pour résoudre un problème A et la machine met n * 1 minutes pour résoudre ce problème A, et si l'humain met environ 5 jours pour résoudre un problème B alors la machine (la meilleure qui soit) devrait mettre environ n * 5 jours pour résoudre ce problème. Je parle ici d'un démonstrateur automatique de théorème étant le plus performant possible, utilisant toutes les astuces que l'homme utile. si n = 100, alors ça n'a aucun interet d'utiliser un tel programme, mais si n = 0,01 ou bien n = 0,000001, alors on a tout interet à utiliser ce programme pour résoudre de nombreux problèmes, même si il resterait encore de nombreux problèmes inaccessibles, peut être à tout jamais.. — Le message qui précède, non signé, a été déposé par Nicobzz (discuter), le Le 21 février 2012 à 14h32

Vois Problème P = NP, cordialement. --Epsilon0 ε₀ 21 février 2012 à 15:08 (CET)

Merci epsilon --Nicobzz (d) 22 février 2012 à 12:05 (CET)

Rebonjour Pierre et epsilon, je vais encore vous déranger, j'en suis désolé, j'aurais une question encore:pensez vous que si il existait, un programme comme décrit ci dessus permettant de résoudre des problèmes mathématiques, sans pour autant résoudre les problèmes quasiment irrésolvables, pourrait être utile? // existe t'il déjà ? (il me semble que les réponse serait oui et non ??)--Nicobzz (d) 4 mars 2012 à 00:54 (CET)