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