P?NP and solution to other complicated mathematical problems

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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.