P vs. NP resistant problems

Question

According to Stephen Cook on wikipedia, http://en.wikipedia.org/wiki/P_versus_NP_problem

...it would transform mathematics by allowing a computer to find a formal proof of any theorem which has a proof of a reasonable length, since formal proofs can easily be recognized in polynomial time. Example problems may well include all of the CMI prize problems.

This opinion seems to suggest that if in fact P = NP, then even the most notoriously difficult problems in mathematics would be essentially trivialized. So I am wondering are there any problems that are resistant to becoming 'easy' even if P = NP? For example, according to Cook, none of the seven Clay Mathematics Institute Millennium problems is an example of this.

Answer 1

Maybe I should start by saying that the quote from Cook is convincing. If a useful polynomial time algorithm for NP complete problem will be found then a computer will be able to give us quickly proofs for theorems (admitting not too long proofs) that we are interested to prove (and may eventually prove), as well as much harder questions that we are uninterested to prove and it seems that we will never be able to prove. (Is the shortest proof of FLT has an even number of characters?) This automatic ability to prove may lead to much more understanding of mathematical theorems and phenomena. We can explore if a specific direction to a proof works, try all sort of lemmas. explore surprising connections, etc. This picture gives good reason to believe that $P \ne NP$ but there are even better reasons for that.

There are various reasons to believe that $NP \ne P$ and indeed one reason is that various tasks that look intractable will immediately look much easier compared to what we experience and expect. The connection with proving specific mathematical theorems looks artificial from various reasons. Usually, to transform a mathematical task into a decision problem to which the NP=?P problem is relevant we need to add a statement like "Is there a proof for RH with less than n pages". This addition makes the original problem much harder. We have a proof for FLT but probably we will never be able to answer the question "what is the smallest number of characters in a proof of FLT?". Fortunately we find the later question uninteresting. So overall Cook's statement can be seen as a provocative agument for why $NP \ne P$, which has some merit, But I dont think it offers any useful connection,

One argument against the connection of real life mathematical proofs and the NP/P gap goes as follows. The NP/P problem is about the effort needed to find a proof compared to the effort needed to verify a proof. Now think about ourselves as computational devices and about this gap for cases of proven theorems. Try to estimate the amount of effort that it takes you to verify a proof which capture n journal pages (or n words) compared to finding such a proof. Is it superlinear in n? more than Quadratic in n? This gap (sometimes referred to as the creativity gap) does not seem similar to the gap between finding a proof and verifying a proof in the NP/P theory (say, the gap between finding a hamiltonian cycle in a large graph or verifying that a certain list of vertices and edges form a Hamiltonian cycle.) We can also talk bout the human effort needed to produce an n-page (or n characters) proof. This effot is on average (for cases of success) probably monotone in n, perhaps superlinear in n but there is no reason to expect it to be exponential in n.

Just to make the main point clear: Deciding mathematical problems including famous ones appears to be by far easier than solving NP-complete problems, and therefore the $NP \ne P$ by itself seems to offer little explanation for the difficulty in solving mathematical problems. But computational complexity insights do give some understanding of this difficulty.

You could have asked a similar question about computability.

Does the fact that there are mathematical statements that are undecidable give some explanation why some mathematical conjectures are so hard to prove? (Well, it gives some indirect explanation of a sort, but not a real useful connection.)

It is an interesting question why proving mathematical conjectures does not seem to be computationally intractable at least for surprisingly many cases where people succeeded. (Also undecidability enters the scene rather rarely.) I am not aware of a very good answer to this question. It may have something to do with what we regard as "interesting" in mathematics, to the nature of mathematical understanding, and to the highly structured nature of mathematical problems.

Answer 2

Preamble: I'm going to make this CW, since there is a good chance that I will misrepresent the exact argument, since I'm working mostly from what I've read here. If you see something in need of fixing, please take advantage of the CW mode.

In particular, most of what I am writing about already appears in Andreas Blass's answer linked below in some form or another, I'm just rewriting it in an attempt to cross some t's and so on.

The Answer

The argument in this answer runs as follows: fix yourself a length for your target proof, $n$. Then if $P=NP$, you will be able to tell in polynomial time whether your statement has a proof of length at most $n$, because that's an $NP$ kind of statement (here, I find it really helpful to think of $NP$ in terms of existential quantification). So $P=NP$ would not be enough to know if there is a proof of any length, but presumably if the proof length is very long, you can't really claim to understand it (think four color theorem). On the other hand, if you know there is a short proof, you might be tempted to find it exhaustively. (And, as Andreas Blass points out in the answer I linked to, this would give you the first available proof in some lexicographical ordering, not necessarily the most enlightening one.)

[Added: As Daniel Litt points out in the comments, having the program terminate with a "Yes" is enough to prove that the theorem is true. I still imagine we might want a more explicit proof, though obviously this is just an opinion and others definitely disagree.]

Note that this ought to apply to any statement that you can formalize, so the answer to your original question would be more or less "No", there are no truly hard statements, just some that have longer shortest proof than others. (That should include statements for which the shortest proof is astronomically long, by the way, but again, those are beyond comprehension.)

Why I don't really buy it

[Added: The quote says that this possibility ...would transform mathematics, but I don't really imagine that it would revolutionize the way we do mathematics in the short term, for the reasons explained below.]

I've played fast and loose with the setting so far, and this is where I believe the statement is a lot weaker than it appears at first. The way I see it, there are two ways of going about this:

1. Encode your theorem and proof in some fixed axiom system. But then, your proof may have to contain a huge chunk of already-known mathematics. So you would have to pick a very large $n$, which is unproductive since you're only interested in a very long proof with very little that's new.
2. Find a way to encode in "currently known mathematics" if possible. On top of the massive overhead that it implies, the biggest issue I see is that your answer would just be a snapshot at time T. You might not be able to write a proof of GRH in 30 pages in 2011, but in 2012, you will have hundred of thousands of pages of fresh math that you can use but don't have to count against your own page total.

That's why I don't see Cook's argument as having a real practical impact, cute as it may be. If I'm overlooking something major, please don't hesitate to correct this. Again, computational complexity is not really my field.

Answer 3

Richard Borcherds gave an example in another thread, of a statement that is (almost) obviously true, but very hard to prove: chess is not a forced win for black. The issue is that (generalized) chess is PSPACE-hard (formalizing the idea of a forced win requires(?) a series of alternating quantifiers, one for each move), and showing a forced win or draw for either side would seem to require surveying the entire game tree which is enormous. So this is almost certainly outside NP. (On the other hand, even P != PSPACE is still unknown).