$NP$ versus $coNP$

The question asks whether $NP$ is closed under complementation: writing $coNP$ for the class of languages whose complements lie in $NP$, is $NP\ne coNP$? The problem crystallized around 1971 alongside the theory of $NP$-completeness, and no single first statement is documented. Its logical face was made precise by Cook and Reckhow, who showed that $NP=coNP$ holds if and only if there is a propositional proof system in which every tautology has a polynomial-size proof [CookReckhow1979].

Since $P$ is closed under complementation, $NP\ne coNP$ would immediately give $P\ne NP$, so the question is at least as hard as the central separation. The Cook–Reckhow correspondence launched propositional proof complexity: superpolynomial lower bounds are known for various concrete proof systems, but not for all systems simultaneously, which is what $NP\ne coNP$ demands [AroraBarak2009].

The problem is open. A resolution requires either a lower-bound technique general enough to defeat every polynomially bounded proof system, or, contrary to expectation, uniformly short certificates of unsatisfiability.