Comment by Xcelerate | Hacker News Reader

Comment by Xcelerate | Hacker News Reader

Parent Full thread

I’m not up-to-date on how advanced proof assistants have become, but are we not nearing the point where serious attempts at proving P vs NP can be automatically validated (or not) by a widely vetted collection of Lean libraries?

The P vs NP problem is expressible as the question of whether a specific Π_2 sentence is true or not (more specifically, whether a particular base theory proves the sentence or its negation). Unlike problems involving higher order set theory or analytical mathematics, I would think any claimed proof of a relatively short arithmetical sentence shouldn’t be too difficult to write up formally for Lean (although I suppose Fermat’s Last Theorem isn’t quite there either, but my understanding is we’re getting closer to having a formal version of it).

The impact of this would be that journals could publicly post which specific sentences they consider to represent various famous open problems, and a prerequisite to review is that all purported proofs require a formal version that automatically Lean-validates. This would nix the whole crank issue.

Then again, I may be way off base with how close we are to achieving something like I’ve described. My impression is that this goal seems about 5 years away for “arithmetical” mathematics, but someone better in the know feel free to correct me.

The effort from going to a paper proof, even one that everyone agrees is correct, to a formally verified one is still gigantic. Requiring all submissions in maths papers to come with a verified Lean proof would be a complete non-starter - most mathematicians don't even use Lean.

In many cases, the problem isn't that the statement of the theorem can't be properly expressed in Lean. It's very easy to write down the statement of FLT in Lean, for example. But for theorems whose proofs have been elusive for decades or centuries, the proofs very likely include objects in rather advanced mathematics that are not at all easy to encode in Lean. This is one of the current struggles of the FLT formalisation process, for example.

In any case, the problem in this case has nothing to do with formalisation, it's simply a case of a bad submission that for unclear reasons didn't get properly peer reviewed.

Thanks for sharing! I didn’t think about all of the intermediate steps that might be difficult to encode, but that makes sense.

I think it's reasonably clear at this point that an elementary proof that P != NP is unlikely to exist; in all likelihood such a proof would have to traverse many other fields of mathematics to get back to the main result, and would almost certainly hinge on areas of mathematics that have proven difficult to formalize so far.

The problem is this: a proof of P ≠ NP is likely to appeal to some theorem in some area of mathematics. Whether or not that theorem has already been formalised is actually unimportant, because it's already accepted as convincing. But the core of the proof would be some sort of a reduction from P ≠ NP to that theorem, and that reduction is likely to be novel and very arduous to formalise.

Reply on news.ycombinator.com