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.