19
$\begingroup$

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?
$\endgroup$
  • 9
    $\begingroup$ Proof assistants are impractical currently. They require a huge amount of effort and expertise to use. $\endgroup$ – Yuval Filmus Jul 30 at 21:11
  • 4
    $\begingroup$ Also, in principle, there are software that can find proofs to every provable statement: the possible proofs are enumerable and can be checked, so it suffices to iteratively check each candidate proof until a valid proof is found. $\endgroup$ – Steven Jul 30 at 21:29
  • 13
    $\begingroup$ @YuvalFilmus I won't say they're easy to use – proving stuff in Coq tends to take me 3× - 10× as long as proving it by hand. But “impractical” is a bit of an overstatement. Really the problem isn't so much that the assistants are impractical, but that they force you to make all the annoying technical-detail assumptions explicit that we otherwise tend to take for granted unquestioningly. $\endgroup$ – leftaroundabout Jul 31 at 7:14
  • 6
    $\begingroup$ Many "proofs" contain bits that are so bad, they are not even wrong. You read it, and then you say "WTF"? That's where conversion to a proof assistant stops. $\endgroup$ – gnasher729 Jul 31 at 15:31
  • 1
    $\begingroup$ @leftaroundabout It doesn't force the author to do anything. They didn't do the work to arrange the proof for a proof assistant. Their argument will be "my proof is so elegant and clever, that's why you don't understand how to state it in a proof assistant". $\endgroup$ – gnasher729 Aug 1 at 22:02
23
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • 6
    $\begingroup$ The last paragraph of (1) is the right answer. Most presumptive proofs are by cranks and a simple test of their crankyness serve as test and is more cost effective. When an argument appears that passes sufficient revisions by experts, I am sure many will be motivated to formalize and verify it automatically. $\endgroup$ – plop Jul 31 at 10:30
  • 2
    $\begingroup$ What do you think of the argument made in my answer that it's likely any proof will rely on lots of prior results, and you'd first have to formalize everything that the paper relies on (every result taught in an undergraduate or graduate course on CS theory, every prior paper that is implicitly relied upon, etc.), and that might take many person-years to do? $\endgroup$ – D.W. Jul 31 at 15:40
  • 2
    $\begingroup$ @Joshua This is news to me, do you have a reference for this? $\endgroup$ – jmite Jul 31 at 17:06
  • 4
    $\begingroup$ @Joshua That's because the theorem is stated for that case. Real-life exceptions such as exclaves, Moon colonies, distinctive water colouring, a higher-genus planet, etc. are excluded from the formulation of the theorem because it is quite obvious that these features introduce counterexamples $\endgroup$ – Hagen von Eitzen Aug 1 at 12:03
  • 3
    $\begingroup$ @D.W.: There's nothing stopping you from formally proving a theorem of the form "if X,...,Y hold then P≠NP" where X,...,Y are previously published theorems. So your 'argument' that you would have to formalize all prior knowledge that the proof relies on does not hold water. If really such a formal proof is found by anyone, it would be much easier for experts to check whether X,...,Y are indeed correct than to check a convoluted poof. The whole point is not to formalize all needed mathematical knowledge but just the part that people most need verification of. $\endgroup$ – user21820 Aug 1 at 15:10
10
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ If we have a P algorithm (i.e. of SAT), we can use proof asst. to prove it's correctness (by induction?). Wouldn't it be an equivalent to verifying a P vs NP proof with a proof asst.? $\endgroup$ – ABD Jul 31 at 2:12
  • 3
    $\begingroup$ @ABD, good point. Possibly -- if the proofs is a proof of P=NP (this doesn't help for P$\ne$NP), and if the proof works by exhibiting a polynomial-time algorithm for some NP-complete problem (this doesn't help if it is a non-constructive proof), and if the proof of correctness for this algorithm is simple. I suspect that any such algorithm will require a non-trivial proof of correctness, in which case we are back to square one, and the comments in my answer apply. $\endgroup$ – D.W. Jul 31 at 2:16
  • 10
    $\begingroup$ "about a day of effort per page of human-written proof". That would be a fairly standard parsing speed for a human in many fields. $\endgroup$ – SE - stop firing the good guys Jul 31 at 10:17
  • $\begingroup$ @SE-stopfiringthegoodguys, sure, but see my point about having to first formalize all of the tens of thousands of prior results that the new paper relies on. (Also see the comment about another study suggesting the cost might be more like a week per page.) $\endgroup$ – D.W. Jul 31 at 15:38
  • $\begingroup$ Thanks for updating your post! By the way, one more reason to formalize known or new mathematics in such conditional theorem form is that it makes it modular. As I am sure you know, modularity means that you can focus your attention on a part that you want to without having to look at other parts. This is why there are many results of the form ( RH ⇒ Q ) where RH is Riemann's hypothesis. Despite RH not being proven yet, these results actually lend weight to the importance of focusing on RH. Of course we hope not to find ¬RH in the end. =) $\endgroup$ – user21820 Aug 2 at 3:04
6
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ Has any one tried by auto? $\endgroup$ – cody yesterday
3
$\begingroup$

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?

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ We could ask whether Wiles' proof for Fermat's Last Theorem can be verified by any software. I know it can't be verified by me :-) $\endgroup$ – gnasher729 Aug 2 at 21:19
  • 1
    $\begingroup$ @gnasher729 From cs.rug.nl/~wim/fermat/wilesEnglish.html: "I expect the problem [of verifying a proof of FLT] to be solved in around fifty years, with a very wide margin. On this page, I try to explain some aspects of the problem, and to give relevant links to the literature and to other web pages." $\endgroup$ – Alexey Romanov yesterday
  • $\begingroup$ "In the spirit of a long and strong Dutch tradition." <-- !! $\endgroup$ – einpoklum yesterday

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.