P?NP and solution to other complicated mathematical problems

In his blog entry here, Lance Fortnow, suggests:

P = NP would also have big implications in mathematics. One could find short fully logical proofs for theorems but these fully logical proofs are usually extremely long. But we can use the Occam razor principle to recognize and verify mathematical proofs as typically written in journals. We can then find proofs of theorems that have reasonably length proofs say in under 100 pages. A person who proves P = NP would walk home from the Clay Institute not with one million-dollar check but with seven.

I am a bit perplexed about his statement. Does it imply that a positive solution to P?NP problem will lead to construct of a 'mechanical proof generator'? If yes, then how?

As far as I understand, the difficulty in construction of such a generator has already been laid out well by Godel and company.

-
–  Kaveh May 8 '11 at 4:17

The problem of deciding whether a string describes a valid proof of a given proposition $T$ in some logical system (say, ZFC) is in NP, since recognizing such a proof takes polynomial time in the size of the proof. If P = NP, it follows that this problem admits a polynomial-time solution, which means it is possible to find a proof of $T$ (if it exists) in time polynomial in the size of the shortest proof, not in the size of $T$.

On the other hand, the fact that the halting problem is unsolvable implies that the maximum length $L_n$ of the shortest proof of a proposition with $n$ symbols is not a computable function, so it eventually grows extremely quickly.

-
Although it is understandable, for sake of clarity I must say that using $P$ to denote the proposition as well as "P" to denote the complexity class is not a good practice. Since "P" is a standard name, it would be wise to use a different letter to denote the proposition. –  Asaf Karagila May 6 '11 at 19:22
...which, to clarify as an answer to the OP, means that Lance should have said 'could' instead of 'would'. (no one knows if any of those 6 other problems have short proofs. –  Mitch May 10 '11 at 3:52

I think his point is, the act of checking a proof of length $\leq N$ is polynomial in $N$(*), so if we want to answer the questions: "Does statement $S$ have a proof of size $\leq N$?" is NP. Hence, if $P=NP$, we could, in polynomial time determine if a theorem has a "human-like" proof - a proof less than some size $N$.

(*) But is this true? Each step in a proof can reference any prior conclusion in a proof, and the proof checker has to skip back to those prior steps to make sure that the new step is valid. It is not obvious to me how checking a proof of length $N$ can be done in polynomial time.

-
Thomas: each step in the proof is the application of some rule to already-proved statements. Those prior steps are known valid, so they don't have to be rechecked. Even in a worst-case scenario, each step in your length-$N$ proof can only depend on $N-1$ previous statements, so your checking is $O(N^2)$, and it shouldn't even be too hard to make it $O(N)$. –  Steven Stadnicki May 6 '11 at 23:59
Well, that's a bit obtuse. Yes, we've validated all the prior statements, but a Turing machine has finite state, so if I say at step 1000 that I am concluding X because step 3 concluded "Y implies X" and step 500 concluded "Y", you have to go back and make sure that those conclusions were actually made on those steps. –  Thomas Andrews May 7 '11 at 1:48

What Godel and co. showed is that there is not always a proof for every claim we wish to verify (or rather, that once we fix our proof system and axioms, something will slip from this specific proof system).

However, we still believe (and base it on our mathematical experience) that the vast majority of mathematical problems can be solved via a proof in our standard proof system. Moreover, we expect such proofs to be of a reasonable size - say, no more than 1,000 pages. We expect proofs to be relatively easy to check. This yields the following question (already laughed at in "Gullivar's Travles", sort of) - why not read all the possible English-written texts up to 1,000 pages, and see if one of them is a valid proof for the claim you wish to prove? After all, checking if a given text is a proof is easy...

The problem is, of course, that the number of 1,000 page long English texts is astronomical. So it takes too much time going over all possible proofs; we need to use some better "search techniques". Usually it means we need to know math and something about the claim in order to find the correct proof.

P=NP will imply that there is an excellent, extremely fast search technique that relies on nothing more than our ability to recognize a valid proof. So anything that is provable, will indeed be proven quite easily, as long as reading the proof is easy as well.

-
You are forgetting that we keep allowing more and more theorems. For example consider the very short proof of Andreas Blass that if every vector space has a basis then the axiom of choice follows. It is a 2.5 pages long proof. It uses theorems which were proven over a nonzero length, and so on and so on. So by the time you reach the "full proof from the ZF" you may have crossed the 100,000 pages (unlikely in this case, but my points remains valid). I can read a 2.5 pages and it will encompass enough material for me to be able to believe this proof. (cont...) –  Asaf Karagila May 6 '11 at 19:40
(...) So the thing is that although we want the proof to be reasonably short, we allow replacing previous theorems by a few lines, instead of full and complete proofs every time. This allows a growth in the length of proof which we may consider reasonable, and we also want to be able to consider. –  Asaf Karagila May 6 '11 at 19:41
Such a growth is only of a linear size - not problematic from a complexity point of view. –  Gadi A May 7 '11 at 7:44
Is it? Suppose I write a 1,000 pages paper using 1,000 theorems each has a 1,000 pages proof, using 1,000 theorems, and so on. This Doesn't seem very linear to me. –  Asaf Karagila May 7 '11 at 7:51
But P=NP does not essentially render us with an "extremely fast technique." P may equal NP, but still require considerable time. –  check123 May 7 '11 at 10:19