<p>Dana has answered the question. But here are some comments on the practical side.</p>

<p>Note that it is undecidable to check if a given sentence is provable in ZFC. $P=NP$ has no consequence on this. $P=NP$ (in fact $P=coNP$) means it is easy to find proofs for <strong>propositional tautologies</strong>, not first-order sentences like GC.</p>

<p>It is $NP$ to check if there is a proof of a given sentence of given length $l$ (in unary) in a fixed theory (e.g. ZFC). So if $P=NP$, then there is a polytime algorithm to check this. Taking $l$ to be some fixed polynomial in the length of the sentence will result in a polytime algorithm.</p>

<p>Practically (this is mentioned by Godel in his famous letter to von Neumann): if $P=NP$, then there is a polynomial time algorithm that given a first-order sentence and $l$ (in unary), the algorithm can find if the sentence has a size $l$ proof in ZFC. Godel's idea was that in this case, if the equivalence $P=NP$ is really feasible (i.e. the algorithm is not just $P$ but is in say $DTime(n^2)$), then one can take this algorithm and run it to check for proofs of feasible but very large length which is going to be larger than any proof any human can ever come up with, and if the algorithm does not find an answer, then the sentence is <em>practically</em> impossible to prove. The trick Dana has mentioned will also work here to find the proof.</p>

<p>For practical means:</p>

<ol>
<li><p>$P=NP$ is not enough, we need the algorithm to be feasible in practice, an algorithm in $DTime(10000n^{10000})$ would not help.</p></li>
<li><p>it will find a proof only if there is one (i.e. the sentence is not an undecidable sentence in ZFC), moreover the proof should be feasibly short.</p></li>
<li><p>it can be the case that $P\neq NP$, but we can still find these feasible proofs algorithmically, for example if $NP=DTime(n^{\log^* n})$.</p></li>
</ol>

CC BY-SA 2.5
2010-11-08T21:54:01.397Z
2010-11-08T22:29:13.707Z
2010-11-08T22:29:13.707Z
Kaveh
<p>Indeed!</p>

<p>If P=NP, not only we can decide whether there exists a proof of length n for Goldbach's Conjecture (or any other mathematical statement), but we can also find it efficiently!</p>

<p>Why? Because we can ask: is there a proof conditioned on the first bit being ..., then, is there a proof conditioned on the first two bits being ...., and so on...</p>

<p>And how would you know n? You'll just try all possibilities, in increasing order. When we make a step in the i'th possibility we also try a step in each of the possibilities 1..(i-1).</p>

CC BY-SA 2.5
2010-11-13T09:25:46.113Z
Isn't this Levin's universal search algorithm?
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-11-13T15:46:29.103Z
@turkistany: yes, it is!
Dana Moshkovitz
CC BY-SA 2.5
2010-11-08T20:44:25.700Z
2010-11-08T20:44:25.700Z
Dana Moshkovitz
<p>This is a naive question, out of my expertise; apologies in advance.</p>

<p>Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For example, Cook's paper "Can Computers Routinely Discover Mathematical Proofs?" formulates
that conjecture as</p>

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

<p>If we restrict attention to polynomially-long proofs, then theorems with such proofs are in NP.
So if P=NP, we could determine whether e.g. Goldbach's Conjecture is true in polynomial time.</p>

<p>My question is: Would we also be able to exhibit a proof in polynomial time?</p>

<p><b>Edit</b>. As per the comments of Peter Shor and Kaveh, 
I should have qualified my claim that we could
determine if Goldbach's conjecture is true if it indeed is one of the theorems with a short proof.  Which of course we do not know!</p>

CC BY-SA 2.5
2010-11-08T20:50:58.590Z
GC seems more like a \Pi_2 problem, since there's an NP predicate (the existence of primes r and s such that n = r+s) and a forall quantification around it. Maybe a weaker conjecture than P vs NP might be enough then ?
Suresh Venkat
CC BY-SA 2.5
2010-11-08T21:40:09.400Z
First, in order to exhibit a short (<1000 pages?) proof of Goldbach's conjecture, there has to be a short proof. P=NP has no bearing on that.
Peter Shor 
CC BY-SA 2.5
2010-11-08T22:00:16.143Z
@Suresh, @Kaveh: You seem to be getting this wrong. Here we have a concrete instance of an NP search problem. The quantifier that is relevant here is the existence of a _proof_ (in a suitable formal system) of the theorem.
Kristoffer Arnsfelt Hansen
CC BY-SA 2.5
2010-11-08T22:03:56.067Z
@Peter: Thanks, yes, I am aware that there are short theorems with arbitrarily long proofs, which is why I tried to reduce attention to those theorems with short proofs.  So, yes, if it turns out that Goldbach's Conj. has no short proof, it falls outside of my question.
Joseph O'Rourke
CC BY-SA 2.5
2010-11-08T22:30:21.193Z
Another remark is that we can actually write down an algorithm, that if P=NP will find a proof to a given statement if it exists in time polynomial in the length of the statement and the length of the shortest proof. (this polynomial is a bound which holds for all theorems), It will be an "astronomical" algorithm however.
Kristoffer Arnsfelt Hansen
CC BY-SA 2.5
2010-11-08T22:46:01.867Z
@Kristoffer Arnsfelt Hansen: I see, GC is an example of possible sentences to be given to the algorithm. I removed my previous comment. Thanks.
Kaveh
CC BY-SA 2.5
2010-11-09T01:47:01.937Z
@Kristoffer: Yes, I like your summary remark!
Joseph O'Rourke
CC BY-SA 2.5
2010-11-09T06:58:41.453Z
@Suresh: GC is Π_1, because the existential quantifiers are bounded by *n*.
Charles Stewart
CC BY-SA 2.5
2010-11-09T07:34:20.997Z
@Charles, Kristoffer: my silly error. Thanks for the correction - I forgot that $n$ is bounded in the sentence.
Suresh Venkat
CC BY-SA 2.5
2010-11-09T12:40:33.657Z
@Kristoffer: What do you mean by an "astronomical" algorithm?  Wouldn't the algorithm be essentially what Dana suggested?
Joseph O'Rourke
CC BY-SA 2.5
2010-11-09T15:50:19.343Z
@Joe: No, I can actually write the algorithm down right now! (Even not knowing if P=NP). The idea is what is known as Levin's Universal search.
Kristoffer Arnsfelt Hansen
CC BY-SA 2.5
2010-11-09T21:22:56.210Z
@Kristoffer: Cool! Didn't know about LS. I see that Marcus Hutter has an improvment of sorts on LS:  "The Fastest and Shortest Algorithm for All Well-Defined Problems." International Journal of Foundations of Computer Science, 13(3):431-443, 2002.
Joseph O'Rourke
<cc.complexity-theory><proof-complexity><automated-theorem-proving><proof-search>
If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?
Joseph O'Rourke
# If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?

(Asked by: username_0 on 2010-11-08)

This is a naive question, out of my expertise; apologies in advance.

Goldbach's Conjecture and many other unsolved questions in mathematics can be written
as short formulas in predicate calculus.
For example, Cook's paper "Can Computers Routinely Discover Mathematical Proofs?" formulates
that conjecture as

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

If we restrict attention to polynomially-long proofs, then theorems with such proofs are in NP.
So if P=NP, we could determine whether e.g. Goldbach's Conjecture is true in polynomial time.

My question is: Would we also be able to exhibit a proof in polynomial time?

**Edit**. As per the comments of Peter Shor and Kaveh,
I should have qualified my claim that we could
determine if Goldbach's conjecture is true if it indeed is one of the theorems with a short proof. Which of course we do not know!

**Tags:** cc.complexity-theory, proof-complexity, automated-theorem-proving, proof-search
> **Comments:**
> **username_1**: GC seems more like a \Pi_2 problem, since there's an NP predicate (the existence of primes r and s such that n = r+s) and a forall quantification around it. Maybe a weaker conjecture than P vs NP might be enough then ?  
> **username_2**: First, in order to exhibit a short (<1000 pages?) proof of Goldbach's conjecture, there has to be a short proof. P=NP has no bearing on that.  
> **username_3**: @Suresh, @Kaveh: You seem to be getting this wrong. Here we have a concrete instance of an NP search problem. The quantifier that is relevant here is the existence of a _proof_ (in a suitable formal system) of the theorem.  
> **username_0**: @Peter: Thanks, yes, I am aware that there are short theorems with arbitrarily long proofs, which is why I tried to reduce attention to those theorems with short proofs.  So, yes, if it turns out that Goldbach's Conj. has no short proof, it falls outside of my question.  
> **username_3**: Another remark is that we can actually write down an algorithm, that if P=NP will find a proof to a given statement if it exists in time polynomial in the length of the statement and the length of the shortest proof. (this polynomial is a bound which holds for all theorems), It will be an "astronomical" algorithm however.  
> **username_4**: @Kristoffer Arnsfelt Hansen: I see, GC is an example of possible sentences to be given to the algorithm. I removed my previous comment. Thanks.  
> **username_0**: @Kristoffer: Yes, I like your summary remark!  
> **username_5**: @Suresh: GC is Π_1, because the existential quantifiers are bounded by *n*.  
> **username_1**: @Charles, Kristoffer: my silly error. Thanks for the correction - I forgot that $n$ is bounded in the sentence.  
> **username_0**: @Kristoffer: What do you mean by an "astronomical" algorithm?  Wouldn't the algorithm be essentially what Dana suggested?  
> **username_3**: @Joe: No, I can actually write the algorithm down right now! (Even not knowing if P=NP). The idea is what is known as Levin's Universal search.  
> **username_0**: @Kristoffer: Cool! Didn't know about LS. I see that Marcus Hutter has an improvment of sorts on LS:  "The Fastest and Shortest Algorithm for All Well-Defined Problems." International Journal of Foundations of Computer Science, 13(3):431-443, 2002.  

---

## 2 answers

### Answer by username_6 on 2010-11-08. Score: 28 | Accepted answer

Indeed!

If P=NP, not only we can decide whether there exists a proof of length n for Goldbach's Conjecture (or any other mathematical statement), but we can also find it efficiently!

Why? Because we can ask: is there a proof conditioned on the first bit being ..., then, is there a proof conditioned on the first two bits being ...., and so on...

And how would you know n? You'll just try all possibilities, in increasing order. When we make a step in the i'th possibility we also try a step in each of the possibilities 1..(i-1).

> **Comments:**
> **username_7**: Isn't this Levin's universal search algorithm?  
> **username_6**: @turkistany: yes, it is!  

---

### Answer by username_4 on 2010-11-08. Score: 25

Dana has answered the question. But here are some comments on the practical side.

Note that it is undecidable to check if a given sentence is provable in ZFC. $P=NP$ has no consequence on this. $P=NP$ (in fact $P=coNP$) means it is easy to find proofs for **propositional tautologies**, not first-order sentences like GC.

It is $NP$ to check if there is a proof of a given sentence of given length $l$ (in unary) in a fixed theory (e.g. ZFC). So if $P=NP$, then there is a polytime algorithm to check this. Taking $l$ to be some fixed polynomial in the length of the sentence will result in a polytime algorithm.

Practically (this is mentioned by Godel in his famous letter to von Neumann): if $P=NP$, then there is a polynomial time algorithm that given a first-order sentence and $l$ (in unary), the algorithm can find if the sentence has a size $l$ proof in ZFC. Godel's idea was that in this case, if the equivalence $P=NP$ is really feasible (i.e. the algorithm is not just $P$ but is in say $DTime(n^2)$), then one can take this algorithm and run it to check for proofs of feasible but very large length which is going to be larger than any proof any human can ever come up with, and if the algorithm does not find an answer, then the sentence is *practically* impossible to prove. The trick Dana has mentioned will also work here to find the proof.

For practical means:

1. $P=NP$ is not enough, we need the algorithm to be feasible in practice, an algorithm in $DTime(10000n^{10000})$ would not help.
2. it will find a proof only if there is one (i.e. the sentence is not an undecidable sentence in ZFC), moreover the proof should be feasibly short.
3. it can be the case that $P\neq NP$, but we can still find these feasible proofs algorithmically, for example if $NP=DTime(n^{\log^\* n})$.


---

