Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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!

share|cite|improve this question
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 Nov 8 '10 at 21:40
@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 Nov 8 '10 at 22:00
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 Nov 8 '10 at 22:30
@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 Nov 9 '10 at 15:50
@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 Nov 9 '10 at 21:22
up vote 25 down vote accepted


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

share|cite|improve this answer
Ah, that's clever! Thanks! – Joseph O'Rourke Nov 8 '10 at 20:55
Isn't this Levin's universal search algorithm? – Mohammad Al-Turkistany Nov 13 '10 at 9:25
@turkistany: yes, it is! – Dana Moshkovitz Nov 13 '10 at 15:46

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

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.