Hacker News Reader

Comment by amichail | Hacker News Reader

Stephen Cook writes:

For example, it would transform mathematics by allowing a computer to find a formal proof of any theorem which has a proof of reasonable length, since formal proofs can easily be recognized in polynomial time. Example theorems may well include all of the CMI prize problems. Although the formal proofs may not be initially intelligible to humans, the problem of finding intelligible proofs would be reduced to that of finding a recognition algorithm for intelligible proofs. Similar remarks apply to diverse creative human endeavors, such as designing airplane wings, creating physical theories, or even composing music. The question in each case is to what extent an efficient algorithm for recognizing a good result can be found. This is a fundamental problem in artificial intelligence, and one whose solution itself would be aided by the NP-solver by allowing easy testing of recognition theories.

View on HN

I don't understand how this can be true given Godel's Incompleteness Theorem. The theorem shows that not all true statements in the second order Peano axiomatic system for the integers can be formally proven by a computer. That is, no first order axiomatic system for the integers is rich enough to capture all true statements in the second order system.

The statement, '...allowing a computer to find a formal proof of any theorem which has a proof of reasonable length...' is where the problem lies. How does one determine which statements have proofs of reasonable length? I believe this is tied in with the Halting Problem. You just can't tell when something will be provable formally and when it can't. A proof of P=NP is not going to destroy mathematics.

That ignores the size of the polynomial, doesn't it? If the fastest polynomial-time proof finding algorithm is O(n^50), it's not going to do much good.

I don't think it would be so bad. There's be some constant factor or number where n^50 would always be less than, say n^n after that constant.

Yea, 51, but with n = 40 you are already at the number of atoms in the universe ~10^80. That would leave around 11^50 calculations per atoms in the universe, at 1,000,000 Ghz you are talking about 10^32 seconds which ~ 3 * 10^24 years. Or 10^15 = (1,000,000,000,000,000) times the current age of the universe.

For any calculable n, n^n is less than n^50. Ok, if computing power doubled every year, for the next 200 years we would still not be able do 50^50 calculations. But in 250 years of doubling each year it would be easy.

Wait, he's saying that recognizing a proof in polynomial time makes finding a proof easy? The search space is exponential, and there's no adequate heuristic for a best-first search.

The quote is about the consequences of P = NP.

NP is the set of problems with solutions that are verifiable in polynomial time. If the problem size is n, imagine a non-deterministic Turing machine that can make one of 2 choices at each step. After n steps there are 2^n possible configurations of the machine, and your polynomial time verifier can check each of these configurations (in parallel, thanks to the non-determinism).

So there's n steps for the guessing and O(n^k) steps for the verification, so you've just been through an exponential search space in polynomial time.

That's why exponential search spaces are the bread and butter of NP. And also why many view P = NP as unlikely.

Reply on news.ycombinator.com