Hacker News Reader

Comment by typest | Hacker News Reader

Given how many people have failed to prove P=NP, and how strange the world would look if P did equal NP, it seems very likely that P!=NP. This would also help explain why it's so hard to prove P!=NP -- finding the proof is itself in NP!

Thus, I'm very skeptical of claims that P=NP.

View on HN

“Finding the proof is itself in NP” does not make sense as finding a singular proof is not something that depends on the size of its input, which is what the entire field of algorithmic complexity studies.

It actually does make sense, and is an important idea in complexity theory. In general, the problem of proving an arbitrary claim in ZFC isn't computable (this is just Godel's incompleteness theorem). if you confine your claims to smaller languages, you get smaller complexity classes. For instance, the problem of proving things in the propostional calculus is called BSAT, and is the quintessential NP complete problem.

In general a nice way of thinking about what NP is are the set of formula that have polynomial time checkable proofs.

It's important to remember that P=NP doesn't just imply that P = NP; it implies that P = PH (the polynomial hierarchy). There are a whole series of much harder problems than NP that also are in P if P = NP. Finding proofs is always at least NP hard! Remember, any proof is at least going to include some boolean phrase (this is true and that is true so we get such and such), which is just BSAT, an NP complete problem. In other words, yes. It's very very unlikely.

Umm. All proofs are in NP, not sure how that is relavent.

Nope... it depends on the language you use to write the proof. Agda proofs for instance are in R.

Is it really a proof (in the philosophical sense) if it cannot be verified in polynomial time?

Computing the n-th Ramsey number R(n,n) is doable in exponential time. You can easily brute-force R(4, 4); a perfectly credible proof that takes exponential time! A credible proof must be verifiable in demonstrably finite time -- not necessarily polynomial.

Hard to find =/= hard to verify. Indeed that is the point of NP (which stands for "nondeterministic polynomial" time): solutions must be easy to check.

Sure! Exponential time can be very small in practice. Agda proofs are proofs when the compiler stops churning.

Reply on news.ycombinator.com