Is the P vs NP problem, an NP or co-NP problem?

Question

A few years ago, a youtube channel named hackerdashery, made an extraordinary youtube video explaining P vs NP, in a semi-vulgarized way : https://www.youtube.com/watch?v=YX40hbAHx3s

At 7 minutes and 56 seconds however, he talks about why it is so hard to prove that P $=$ NP or that P $\neq$ NP, and states that proving things is in fact an NP problem (in the video however, he writes down that it is actually a co-NP problem).

Thus, is proving things, in particular P $=$ NP or P $\neq$ NP, an NP or co-NP problem? If so, why? And where could I find more on this?

Answer 1

It isn't meaningful to say that a single specific question is in NP or any other complexity class. In order to classify things as being in P, or NP, or co-NP, etc. they need to be sets of problems with some parameter. So for example, the problem "Is the positive integer n prime" is a question where we can discuss this sort of thing.

In a certain overly pedantic sense, the correct answer to your question is that the problem you care about is in P, since there's an algorithm which will answer every question of your form in polynomial (in fact constant time). But we don't know if that algorithm is just "Return TRUE" or is "Return False."

The idea that the video may be touching on is the idea that if P != NP, then in general, finding proofs is hard. In fact, "Is statement S provable in formal system A with a proof of length at most x" is an NP-hard problem" (Questions in this are things like "Is there a proof of Fermat's Last Theorem that's shorter than 5 pages.") . And we also expect that if P != NP, for most "natural" NP-complete problems, random instances will often not be easy. So if P != NP, then searching for proofs should often be difficult, and thus we shouldn't be surprised that the proof that P != NP would itself be one of those. This may be what they were trying to say.

Answer 2

There are grave conceptual issues at hand here.

Establishing proofs is the aim of mathematics. This is a task carried out by humans, usually using pen (or pencil) and paper. Some amount of coffee might be involved in the process too. This definitely has nothing to do with $\mathsf{NP}$.

Now, "proofs" may be meant in the sense of logic and proof systems. These are procedures with axioms and deduction rules applied to them which yield truthful statements (according to the underlying logic). This is the realm of Gödel's incompleteness theorems and has important connections to computability theory. This, also, has definitely nothing to do with $\mathsf{NP}$.

Then, there is another notion of "proof" in complexity theory, namely that of an interactive proof system (IPS). A prover, generally with unbounded computational capacity, tries to convince a verifier of a statement; the verifier is a limited machine, but which cannot be easily fooled. (Note how this has much more to do with a real-life argument than with a mathematical proof.) It has been shown that the class of decision problems that can be verified by such a system when the verifier is a probabilistic poly-time Turing machine (which is the usual setting) is equal to $\mathsf{PSPACE}$. This does seem to have a bit more to do with $\mathsf{NP}$.

However, $\mathsf{NP}$ does not contain proofs. $\mathsf{NP}$ (as well as any of the classes $\mathsf{coNP}$, $\mathsf{P}$, $\mathsf{PSPACE}$, and so on) contains decision problems. One of the definitions of $\mathsf{NP}$ is that it contains those problems for which one can efficiently (i.e., in poly-time) and determistically verify the solution of yes-instances. In a sense, this is equivalent to an IPS in which the verifier is deterministic and obtains a single message from the prover. You can easily see how this is quite of a restriction to the usual IPS setting.

Thus, if you could say something the likes of "$\mathsf{NP}$ is about proving things," then you could equally say "$\mathsf{PSPACE}$ is about proving things." I do not think this is a particular enlightening way of thinking about it.

Answer 3

Theorem-proving is co-NP-complete :

Depending on the underlying logic, the problem of deciding the validity of a formula varies from trivial to impossible. For the frequent case of propositional logic, the problem is decidable but co-NP-complete, ...
- https://en.wikipedia.org/wiki/Automated_theorem_proving

In a comment, Yuval Filmus did state that the language of propositional tautologies is co-NP-complete, which basically is the same thing, since :

"The most common type of mathematical theorem can be symbolized as p⟹q, where p and q may be compounded statements. To assert that p⟹q is a theorem is to claim that p⟹q is a tautology; that is, that it is always true. We know that p⟹q is true unless p is true and q is false. Thus, to prove that p implies q, we have to show that whenever p is true it follows that q must be true."
- https://math.stackexchange.com/questions/2486302/how-are-theorems-tautologies

I don't know how the problem of P versus NP could be described as propositional logic though, but will update this answer once I know more on this. I did however find this, which might be a step in the good direction :

... the question "is P a proper subset of NP?" can be reformulated as "is existential second-order logic able to describe languages (of finite linearly ordered structures with nontrivial signature) that first-order logic with least fixed point cannot?".
- https://en.wikipedia.org/wiki/P_versus_NP_problem#Logical_characterizations

EDIT : P = NP cannot be written in propositional logic, but can be written in first order logic (as can be seen here : https://math.stackexchange.com/questions/51740/expressing-p-np-as-a-first-order-formula). The language of first order tautologies is PSPACE-complete when considering Boolean variables, and undecidable when considering natural variables. P = NP apparently considers natural variables.