How hard would it be to state P vs. NP in a proof assistant?

Question

GJ Woeginger lists 116 invalid proofs of P vs. NP problem. Scott Aaronson published "Eight Signs A Claimed P≠NP Proof Is Wrong" to reduce hype each time someone attempts to settle P vs. NP. Some researchers even refuse to proof-read papers settling the "P versus NP" question.

I have 3 related questions:

1. Why are people not using proof assistants that could verify whether a proof of P vs. NP is correct?
2. How hard or how much effort would it be to state P vs. NP in a proof assistant in the first place?
3. Is there currently any software that would be at least in principle capable of verifying a P vs. NP proof?

Answer 1

I'm going to disagree with DW. I think that it is possible (although difficult) for a P vs. NP result to be stated in a proof assistant, and moreover, I wouldn't trust any supposed proofs unless they were formalized in this way, unless they came from very reputable sources.

In particular, none of the resources DW states are based on type theory, which is a very promising direction for proof assistants. Coq has been used to formalize the proof of the 4-color theorem among others, so it's clearly capable of some heavy mathematical lifting.

To answer your specific questions:

1. The main reason is that theorem provers aren't widely accepted in the mathematical community. Learning them takes effort, and mathematicians are often skeptical of the underlying techniques (type theory, constructive math, etc.) But there are some fields where leading researchers are very comfortable with making large developments formalized in a proof assistant, like category theory, programming language theory, formal logic, etc. So I think there is as much of a cultural issue as an inherent feasibility issue.

   The other reason is that, so far, most of the purported "proofs" have been by cranks, who don't want to formalize their result because it will inevitably reveal the flaws.

2. It is not hard at all to state P vs. NP in a proof assistant. One could use Turing Machines, but it would probably be easier to model a simple Turing-complete programming language using inductive families to model small-step semantics, and define the run-time as the number of steps a program takes. You could define $P$ as the languages accepted by programs halting in a polynomial number of steps, and $NP$ as languages that can be verified in polytime with a polynomial-length certificate.

   EDIT: It turns out there are existing techniques for showing that algorithms run in polynomial time in a theorem prover. So this could be used either to show a polytime algorithm for an NP-hard problem, or to derive a contradiction from the existence of such an algorithm.

3. There is tons of software that is capable of verifying such a proof, provided the proof was written using that software. The two candidates I'd put the most stock in are Coq and Lean. Coq in particular has been used to verify several major results in mathematics.

Answer 2

Using proof assistants for this purpose is certainly possible in principle, but I suspect it would take more effort than most folks who write such proofs would be interested in putting in. It would require a substantial amount of effort from the author of a purported P vs NP proof to formalize their proof.

Translating a proof written for humans into a format that a proof assistant can verify was tedious and time-consuming. I have seen estimates of between a day to a week of effort per page of human-written proof. Then, one must also formalize all prior results that the proof is building on. When we look at recent attempts at proving P vs NP, they typically use a lot of advanced machinery and sophisticated pre-existing results from prior papers, which would need to be formalized too.

Because of this, I expect it would be completely impractical to formalize both the proposed new proof and the proofs of all prior results that it relies upon, for the kinds of purported proofs we've seen so far. As user21820 points out, what would be more practical would be to formalize only the statement of all prior results that are relied upon, but not their proof. Thus, instead of proving the theorem $T$, we'd formalize a proof that $(X \land Y \land \cdots) \implies T$, where $X,Y,\dots$ are the prior results that the proof relies upon. This falls short of fully verifying the NP-completeness result, but if people have faith in the prior results, it would allow people to gain confidence in the new result. This would be a lot more realistic than formalizing the entire proof of $T$: while it would take some effort to formalize all of the prior results $X,Y,\dots$, it's a lot less than the effort to formalize the proofs of those prior results too.

Still, it would be challenging and require a non-trivial expenditure of effort to formalize a proof, even with this trick.

You can look at existing libraries of theorems in mathematics and computer science that have been formalized and formally verified: see http://us.metamath.org/ and http://formalmath.org/ and https://www.isa-afp.org/topics.html and http://mizar.org/library/. You might notice that a lot of what is formalized there concerns basic undergraduate material. We're a far way from formalizing all theorems taught at an undergraduate level, let alone those taught at a graduate level, let alone new research results.

For more background, see https://math.stackexchange.com/q/792010/14578 and https://math.stackexchange.com/q/113316/14578 and https://math.stackexchange.com/q/1767070/14578 and https://math.stackexchange.com/q/2747661/14578 and http://www.ams.org/notices/200811/tx081101370p.pdf.

Answer 3

I can give a direct answer to (2): $P\ne NP$ has been stated in Lean (along with the other main results of Cook's paper, where the conjecture was first described), as part of the Formal Abstracts project.

Answer 4

I believe your question is not that much of a proper theory question, so with your permission I'll give it a not-so-technical answer.

Why are people not using proof assistants that could verify whether a proof of P vs. NP is correct?

Because CS theorists rarely (perhaps extremely rarely) write proofs in machine-verifiable form.

How hard or how much effort would it be to state P vs. NP in a proof assistant in the first place?

Very hard at least in the "uninteresting" sense that @DW explained; but it could be anywhere from easy to impossible in the "interesting" sense of expressing the concepts in a proof, if it were to exist.

But you know, this will never happen because:

1. Until a proof is found it can't be done anyway
2. You have to know the proof like the back of your hand to convert it into machine-verifiable form.
3. ... and when enough people know the proof, they will either have found a flaw or be satisfied that it's valid and not care about machine-checking it.

Is there currently any software that would be at least in principle capable of verifying a P vs. NP proof?

I'm not well-versed enough in proof verification software to comment about what's actually implemented, but it's probably nearly-impossible to answer your question, because - who knows what form such a proof will take? And thus - how would you know, now, if it's expressible in such a way that your proof verifier can process?