Si P = NP, pourrions-nous obtenir des preuves de la conjecture de Goldbach, etc.?

Ceci est une question naïve, de mon expertise; excuses à l'avance.

La conjecture de Goldbach et de nombreuses autres questions non résolues en mathématiques peuvent être écrites sous forme de formules courtes dans le calcul des prédicats. Par exemple, le document de Cook "Les ordinateurs peuvent-ils découvrir systématiquement des preuves mathématiques?" formule cette conjecture comme

\forall n [(n > 2 \land 2 | n) \supset \exists r \exists s (P (r) \land P (s) \land n = r + s)]

$\forall n [( n > 2 \wedge 2 | n) \supset \exists r \exists s (P(r) \wedge P(s) \wedge n = r + s) ]$

Si nous limitons notre attention aux preuves polynomiales, alors les théorèmes avec de telles preuves sont en NP. Donc, si P = NP, nous pourrions déterminer si, par exemple, la conjecture de Goldbach est vraie en temps polynomial.

Ma question est la suivante: pourrions-nous aussi montrer une preuve en temps polynomial?

Modifier . Selon les commentaires de Peter Shor et Kaveh, j'aurais dû nuancer mon affirmation selon laquelle nous pourrions déterminer si la conjecture de Goldbach est vraie si elle est effectivement l'un des théorèmes avec une preuve courte. Ce que bien sûr nous ne savons pas!

cc.complexity-theory proof-complexity automated-theorem-proving proof-search Joseph O'Rourke
la source

Premièrement, pour pouvoir présenter une courte preuve (<1 000 pages?) De la conjecture de Goldbach, il doit y avoir une preuve courte. P = NP n'a aucune incidence sur cela.

Peter Shor

@Suresh, @Kaveh: Vous semblez vous tromper. Nous avons ici un cas concret de problème de recherche de NP. Le quantificateur qui est pertinent ici est l’existence d’une preuve (dans un système formel approprié) du théorème.

Kristoffer Arnsfelt Hansen

Une autre remarque est que nous pouvons réellement écrire un algorithme, qui si P = NP trouvera une preuve à une déclaration donnée s’il existe en polynôme temporel dans la longueur de la déclaration et la longueur de la preuve la plus courte. (ce polynôme est une borne qui vaut pour tous les théorèmes), ce sera un algorithme "astronomique" cependant.

Kristoffer Arnsfelt Hansen

@ Joe: Non, je peux écrire l'algorithme maintenant! (Même en ne sachant pas si P = NP). L'idée est ce qu'on appelle la recherche universelle de Levin.

Kristoffer Arnsfelt Hansen

@ Kristoffer: Cool! Je ne savais pas à propos de LS. Je vois que Marcus Hutter a quelque peu amélioré LS: "L'algorithme le plus rapide et le plus rapide pour tous les problèmes bien définis." Journal international des fondations de l'informatique, 13 (3): 431-443, 2002.

Joseph O'Rourke

Réponses:

Effectivement!

Si P = NP, non seulement nous pouvons décider s'il existe une preuve de longueur n pour la conjecture de Goldbach (ou tout autre énoncé mathématique), mais nous pouvons également le trouver efficacement!

Pourquoi? Parce que nous pouvons demander: existe-t-il une preuve conditionnée sur le premier bit étant ..., alors, y a-t-il une preuve conditionnée sur les deux premiers bits étant ...., etc.?

Et comment saurais-tu n? Vous allez juste essayer toutes les possibilités, par ordre croissant. Lorsque nous faisons un pas dans la ieme possibilité, nous essayons aussi un pas dans chacune des possibilités 1 .. (i-1).

Dana Moshkovitz
la source

Cet algorithme de recherche universel de Levin n'est-il pas?

Mohammad Al-Turkistany,

@turkistany: oui, c'est ça!

Dana Moshkovitz

Dana a répondu à la question. Mais voici quelques commentaires sur le côté pratique.

Notez qu'il est indécidable de vérifier si une phrase donnée peut être prouvée dans ZFC. n'a aucune conséquence sur cela. (en fait ) signifie qu'il est facile de trouver des preuves pour les tautologies propositionnelles , et non des phrases de premier ordre comme GC. $P=NP$ $P=NP$ $P=coNP$

Il est de vérifier s’il existe une preuve d’une phrase donnée de longueur donnée (unaire) dans une théorie figée (par exemple ZFC). Donc, si , il existe un algorithme polytime pour vérifier cela. Prenant comme un polynôme fixe dans la longueur de la phrase, on obtiendra un algorithme polytime. $NP$ $l$ $P=NP$ $l$

Pratiquement (ceci est mentionné par Godel dans sa célèbre lettre à von Neumann): si , il existe un algorithme temporel polynomial qui donne une phrase du premier ordre et (unaire), l’algorithme peut déterminer si la phrase a une taille épreuve en ZFC. L’idée de Godel était que, dans ce cas, si l’équivalence est réellement réalisable (c’est-à-dire que l’algorithme n’est pas simplement mais est, par exemple, $P=NP$ $l$ $l$ $P=NP$ $P$ $DTime(n^2)$ ), alors on peut prendre cet algorithme et le lancer pour vérifier les preuves de longueur réalisable mais très grande qui sera plus grande que toute preuve que n'importe quel humain puisse jamais trouver, et si l'algorithme ne trouve pas de réponse, phrase est pratiquement impossible à prouver. Le truc que Dana a mentionné travaillera également ici pour trouver la preuve.

Pour des moyens pratiques:

ne suffit pas, il faut que l’algorithme soit réalisable dans la pratique, un algorithme en n’aiderait pas. $P=NP$ $DTime(10000n^{10000})$
il ne trouvera une preuve que s’il en existe une (c’est-à-dire que la phrase n’est pas une phrase indécidable en ZFC); de plus, la preuve devrait être raisonnablement courte.
$P\neq NP$ $NP=DTime(n^{\log^* n})$

Kaveh
la source

(n^{10})

$(n^{10})$