A question that answers itself.

  1. If P=NP could be proved in a formal language, then surely it would be as easy to verify the proof as it would be to discover/derive it? Couldn't a program just quickly check that every sentence/line obeyed the formal rules?

  2. If P!=NP could be proved in a formal language, then it could take a while to do so.

  3. Its taken a while to formally prove either P=NP or P!=NP.

-> So either our language isn't accurate, isn't formal enough or P!=NP?

  • 6
    $\begingroup$ Proofs are typically much harder to discover than to verify. $\endgroup$
    – Juho
    Jul 14, 2021 at 7:12
  • 2
    $\begingroup$ @johnbot this is not even a question. Furthermore, if you believe its so easy to prove that $P=NP$ or $P\neq NP$ then why won't you prove it for yourself? This question is extremely hard (and is not the only hard unanswered question out there). Verifying a proof and finding it are two completely different things. Finding a proof is much much harder $\endgroup$
    – nir shahar
    Jul 14, 2021 at 7:58
  • $\begingroup$ @nirshahar thats exactly what I'm saying. P!=NP is hard to prove because P!=NP is true, and so its harder to prove than to verify. Otherwise, if P=NP it would be easy to prove (which it very clearly isnt, and I'm not suggesting it is). What I mean by the question is that the answer to "Why has it taken so long to prove P!=NP?" is "because P=!NP", i.e. the question answers itself. $\endgroup$
    – johnbot
    Jul 14, 2021 at 9:35
  • 1
    $\begingroup$ If you are interested in discovering proofs in a world where P = NP, search for Impagliazzo's five worlds. $\endgroup$
    – Juho
    Jul 14, 2021 at 10:05
  • 1
    $\begingroup$ @johnbot even if we say that P=NP, we still might not know what algorithms in P are for the NP-complete problems. Not being able to easily proof that P=NP doesn't imply that $P\neq NP$. Your argument is totally nonsense and not formal. This is what is wrong here. The math isn't "not formal enough", and it is very accurate, but still, we don't know the answer to this question. $\endgroup$
    – nir shahar
    Jul 14, 2021 at 10:28

3 Answers 3


Suppose that $\mathsf{P}=\mathsf{NP}$. Your argument seems to be the following: since there exists an algorithm $A$ that is able to check whether a given short proof of mathematical statement is valid then there must exist an algorithm $B$ that decides whether such a short proof exists. Let's use $B$ on the statement $\mathsf{P}=\mathsf{NP}$.

There are several problems with that. First it assumes that $\mathsf{P}=\mathsf{NP}$ in the first place. If we knew that this is true we would have no need to run $B$ on $\mathsf{P}=\mathsf{NP}$.

Second, it assumes that we know $B$ while the above argument only shows that some $B$ must exist. It might be the case that $B$ exists but we don't know it. Moreover, if $B$ existed and we knew it, then $B$ itself would be a proof that $\mathsf{P}=\mathsf{NP}$.

Third: Suppose that $\mathsf{P}=\mathsf{NP}$ (but we don't know it) and that we have some magic candidate algorithm $B$. $B$ is only able to decide whether an input statement admits short proofs. By short I mean proofs whose lengths are upper bounded by $n^c$, where $n$ is the length of the statement, and $c$ is a constant of choice. How do you pick $c$? We don't know how long a proof of $\mathsf{P}=\mathsf{NP}$ is.

Finally, notice that $\mathsf{P}=\mathsf{NP}$ is a specific statement. Therefore, if we assume that "$\mathsf{P}=\mathsf{NP}$" can be proved either true or false, then we already have a constant-time algorithm that settles the matter. Consider the shortest proof written in binary (in some proof language) of "$\mathsf{P}=\mathsf{NP}$" or "$\mathsf{P} \neq \mathsf{NP}$" and let $k$ be its length. Clearly $k$ is a fixed number. We can simply generate all possible proofs in lexicographic order and check whether each of them is a valid proof of either "$\mathsf{P}=\mathsf{NP}$" or "$\mathsf{P} \neq \mathsf{NP}$". Eventually we will reach the proofs of length $k$. There are only finitely many proofs of length at most $k$ (namely $2^{k+1}-1$) and checking each of them requires a time upper bounded by some function $f(k)$. Therefore the overall running time is $O(2^k f(k)) = O(1)$. This constant can be huge and this does not bring us any closer to settling the $\mathsf{P}$ vs $\mathsf{NP}$ question.

  • $\begingroup$ OK interesting, I guess I didn't consider the difference between knowing that B exists and knowing what it actually is. And yes, it is a specific statement, although couldn't you rephrase it as a statement about every problem in P? $\endgroup$
    – johnbot
    Jul 14, 2021 at 13:04
  • $\begingroup$ It would still be one particular statement that you wish to prove. The point is that any single statement that is not undecidable can be automatically proven true or false in constant (but huge) time by the trivial algorithm that enumerates all the possible proofs. If $\mathsf{P}=\mathsf{NP}$ then there is an efficient (polynomial-time) algorithm to find a proof of every statement that admits a proof of length $\ell \le n^c$ (the above naive algorithm would instead take time exponential in $\ell$). Nevertheless, the above facts do not help us figure out whether $\mathsf{P}=\mathsf{NP}$. $\endgroup$
    – Steven
    Jul 14, 2021 at 14:09
  • $\begingroup$ "if [an algorithm (that solves NP complete problems and) that finds a proof for P=NP] B existed and we knew it, then B itself would proof that P=NP [without running it]". That's a very tricky statement. We already know an algorithm B that can find a proof for P=NP in polynomial time, but only if such a proof for P=NP exists: en.wikipedia.org/wiki/… $\endgroup$ Jul 15, 2021 at 0:06

Sometimes a short and easily verifiable proof takes a long time to discover. This may be due to several reasons. Maybe the general consensus in the research community is that the claim is probably not true, and most people who work on it are trying to prove the converse. Maybe it's believed to be too difficult for current techniques, and most researchers prefer to work on easier problems where progress can be made. Maybe finding it requires computer searches that were out of reach of older (or even current) hardware. Maybe it requires some radical new idea.

For a concrete example, take Kaplansky's unit conjecture. It claims that certain classes of generalized polynomials $K[G]$ do not contain nontrivial invertible elements. If this conjecture is false, then there exists such a class $K[G]$ and a nontrivial invertible polynomial $f \in K[G]$. If we are given this $K[G]$ and $f$, it's easy to verify (by computer or on paper) that it disproves the conjecture. The conjecture was stated in 1940 and publicized in the 1950s, and a counterexample was found by Gardam in 2021 using a computer search. He has stated that it ran on his laptop, so it probably would have been in reach of much earlier supercomputers.

Then there's the possibility that $P = NP$ is provably true, but its simplest proof is very long and difficult. Maybe there is a polynomial time algorithm for Boolean satisfiability, but it's extremely intricate and has a running time of $n^{10000}$ or something even more outrageous.


It's important to address the elephant in the room:

Why has it taken so long to prove that P != NP?

This has not been proven.

The argument you have given "does not compute" - it uses terms that simply do not find together.

The one (the question of whether $P$ equals $NP$) and the other (the difficulty of finding a proof for it or its opposite) has nothing to do with each other whatsoever. Since the $O$ notation removes all multiplicative and additive constants, there can be P problems which are arbitrarily difficult to solve, so you can never use the perceived difficulty in finding a solution/proof to argue whether a problem is in $P$ or $NP$, both or none. As a fun example, by some definitions chess is an $O(1)$ problem in $P$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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