37

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!

Joseph O'Rourke
  • 3,753
  • 23
  • 41
  • 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 Nov 08 '10 at 20:50
  • 8
    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 08 '10 at 21:40
  • 4
    @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 08 '10 at 22:00
  • @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 Nov 08 '10 at 22:03
  • 2
    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 08 '10 at 22:30
  • @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 Nov 08 '10 at 22:46
  • @Kristoffer: Yes, I like your summary remark! – Joseph O'Rourke Nov 09 '10 at 01:47
  • 1
    @Suresh: GC is Π_1, because the existential quantifiers are bounded by n. – Charles Stewart Nov 09 '10 at 06:58
  • @Charles, Kristoffer: my silly error. Thanks for the correction - I forgot that $n$ is bounded in the sentence. – Suresh Venkat Nov 09 '10 at 07:34
  • @Kristoffer: What do you mean by an "astronomical" algorithm? Wouldn't the algorithm be essentially what Dana suggested? – Joseph O'Rourke Nov 09 '10 at 12:40
  • 4
    @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 09 '10 at 15:50
  • 4
    @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 09 '10 at 21:22

2 Answers2

28

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

Dana Moshkovitz
  • 10,979
  • 1
  • 50
  • 77
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})$.

Kaveh
  • 21,577
  • 8
  • 82
  • 183
  • 1
    Your point 1. is far too pessimistic. DTIME$(n^{10})$ also wouldn't help! –  Nov 27 '19 at 10:14