If P=NP, could we obtain proofs of Goldbach's Conjecture etc.?

Question

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!

Answer 1

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

Answer 2

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