NP versus coNP Problem

NP versus coNP Problem

Definitions and mathematical statement

For $L\subseteq\{0,1\}^*$ write $\overline L=\{0,1\}^*\setminus L$ and set $\mathsf{coNP}=\{\overline L:L\in\mathsf{NP}\}$. The question is $\mathsf{NP}=\mathsf{coNP}$. A Cook--Reckhow proof system is a polynomial-time computable surjection $P:\{0,1\}^*\to\mathsf{TAUT}$, where $\mathsf{TAUT}$ is the set of propositional tautologies. Polynomial boundedness means \[ \exists\text{ polynomial }q\ \forall\varphi\in\mathsf{TAUT}\ \exists\pi: P(\pi)=\varphi,\quad|\pi|\le q(|\varphi|). \] The equivalent proof-system question permits choosing the system; it is not restricted to a familiar calculus.

Formulation and concept references: [S1].

Short English statement

Does efficient certification of yes-answers always come with efficient certification of no-answers?

Research attempt

Scope, source check, and plan.

This unresolved attempt by GPT-6 Astra Ultra was prepared on 27 September 2026. The process was to check the proof-system formulation, examine a concrete certificate-compression strategy, and construct adversarial examples for conclusions drawn from representation size. No separation or collapse of complexity classes is claimed.

Cook--Reckhow [E1], Propositions 1.1 and 1.4, give the equivalence between $\mathsf{NP}=\mathsf{coNP}$ and existence of a polynomially bounded proof system. Their definition ranges over all polynomial-time surjections onto tautologies. The catalogue's [S3] explicitly restricts its lower-bound target to tree-like semantic systems with bounded line size. The other catalogue research entries are retained as references; their titles are not accepted as proofs of a class equality or separation.

The selected route is to test whether short unsatisfiability certificates can be obtained by eliminating auxiliary variables from a verifier. Parity gives an exact calculation: elimination can require exponentially many clauses, while an elementary algebraic certificate remains short. A separate explicit proof-system construction then tests whether a lower bound in one verifier can possibly quantify over all verifiers.

The universal quantifier over proof systems.

If a proof system $P$ has proofs bounded by a polynomial $q$, a verifier for $\mathsf{TAUT}$ guesses $\pi$ of length at most $q(|\varphi|)$ and checks $P(\pi)=\varphi$. Conversely, if $\mathsf{TAUT}$ has a polynomially bounded NP verifier $V$, define $P(\varphi,w)=\varphi$ when $V(\varphi,w)$ accepts, and output a fixed tautology $\tau_0$ otherwise. This is a polynomial-time surjection with polynomially bounded proofs. Together with coNP-completeness of tautology, this proves the equivalence used here [E1]. Consequently a negative answer requires failure of polynomial boundedness for every such $P$. A positive answer needs just one sound, complete, polynomial-time verifier with a uniform polynomial proof bound.

Lemma 13.1: exact clause complexity of parity.

For $n\ge1$ let \[ E_n=\{x\in\{0,1\}^n:x_1+\cdots+x_n=0\pmod2\}. \] Every CNF on these $n$ variables alone whose satisfying set is exactly $E_n$ contains at least $2^{n-1}$ non-tautological clauses. This bound is attained.

Proof. Remove repeated literals and tautological clauses. Every remaining clause must be true on all even-parity inputs. If a clause omits $x_i$, assign the variables it mentions so as to falsify every literal. Choose the other unspecified variables arbitrarily except $x_i$, and choose $x_i$ last to make the total parity even. This gives a satisfying input of $E_n$ falsifying the clause, a contradiction. Thus every such clause mentions all $n$ variables. With no repeated or complementary literals, it is falsified by exactly one assignment; that assignment must have odd parity. All $2^{n-1}$ odd assignments must be excluded, giving the lower bound. Conversely, for each odd assignment take the width-$n$ clause falsified precisely by it. Their conjunction defines $E_n$.$\square$

The result also holds for odd parity, by exchanging the final parity bit. It is a lower bound on an exact visible-variable representation, with no hypothesis about how that representation is generated. It therefore falsifies any proposed universal procedure that projects an arbitrary short CNF onto its visible variables and always returns a polynomial-size equivalent CNF without new variables.

A short extended representation, checked gate by gate.

Introduce prefix variables $p_0,\ldots,p_n$, require $p_0=0$, and impose \[ p_i=p_{i-1}+x_i\pmod2\quad(1\le i\le n). \] Each relation $c=a+b\pmod2$ is given by the four clauses \[ (a\vee b\vee\neg c),\quad (a\vee\neg b\vee c),\quad (\neg a\vee b\vee c),\quad (\neg a\vee\neg b\vee\neg c). \] They exclude exactly the four triples violating the XOR equation. The unit clauses $\neg p_0$ and $\neg p_n$ complete a CNF with $4n+2$ clauses. For every input $x$, the gate equations determine a unique sequence $p_i$; its final value is the parity of $x$. Thus existentially projecting the $p$ variables gives exactly $E_n$. With binary variable indices, the encoded length is $O(n\log(n+2))$.

The exponential lower bound is consequently not a statement that parity requires long descriptions, or that checking parity is difficult. It records the cost of requiring a particular description after forgetting the internal prefix values. This distinction matters in proof search: a short proof can retain useful intermediate variables instead of projecting them away.

Lemma 13.2: short certificates for affine inconsistency.

Let $A\in\mathbb F_2^{m\times r}$ and $b\in\mathbb F_2^m$. The system $Az=b$ is inconsistent if and only if there is $\lambda\in\mathbb F_2^m$ with \begin{equation}\label{wsref-0-61-31-33-3a-64-75-61-6c} \lambda^{\mathsf T}A=0, \qquad\lambda^{\mathsf T}b=1. \end{equation} This is an $m$-bit certificate checked in $O(mr+m)$ field operations.

Proof. Such a certificate would transform a hypothetical solution into $0=1$, so it proves inconsistency. Conversely apply Gaussian row elimination to the augmented matrix $(A\mid b)$, tracking each row operation on an additional identity matrix $I_m$. If elimination never produces a zero coefficient row with right side $1$, assign free variables arbitrarily and solve the pivot equations backwards, obtaining a solution. In the inconsistent case there is therefore a row $(0\mid1)$; the corresponding tracked row of the identity matrix is $\lambda^{\mathsf T}$. Row operations preserve the stated linear-combination interpretation. All matrices and all operations have polynomial size.$\square$

Apply this directly to two prefix encodings on the same $x$ variables, with $p_0=q_0=0$, respective equations \[ p_i+p_{i-1}+x_i=0,\qquad q_i+q_{i-1}+x_i=0, \] and the incompatible requirements $p_n=0$, $q_n=1$. Sum every displayed prefix equation and all four boundary equations. Each $x_i$ occurs twice; every internal $p_i,q_i$ occurs twice; the boundary occurrences also cancel. The right side is $1$. Thus the all-ones row-combination vector is already an explicit certificate for $0=1$. It has $2n+4$ bits.

A procedure that first expands both projected parity conditions into CNF would generate exponentially many clauses before noticing their conflict. The affine certificate avoids that expansion. This demonstrates why the representation lower bound in Lemma 13.1 cannot by itself lower-bound proof length across all proof systems.

Where the algebraic upper-bound proposal breaks.

Boolean circuits do not consist only of XOR relations. Over $\mathbb F_2$, an AND gate has equation $z+xy=0$. Treating the monomial $xy$ as an independent linear variable discards its relation to $x$ and $y$. There is an immediate counterexample: the equations \[ x=0,\quad y=0,\quad z=1,\quad z=xy \] are inconsistent, but replacing $xy$ by a free variable $u$ gives the consistent affine system $x=0,y=0,z=1,z=u$. Therefore affine inconsistency certificates remain sound for the affine systems to which they apply, but this naive linearization is incomplete for Boolean gate systems. Restoring $u=xy$ restores the nonlinear constraint. No polynomial bound for certificates handling every such nonlinear system is proved here.

An explicit stress test for proof-system lower bounds.

There is also a simple way to make the quantifier failure concrete. Define a truth-table proof system $T$: a well-formed proof contains a formula $\varphi$ and the evaluations on all assignments in a fixed order; $T$ checks the table and outputs $\varphi$ if all entries are $1$. Otherwise it outputs $\tau_0$. The checker first verifies that the supplied table length is exactly $2^v$, where $v$ is the number of distinct variables. It performs the exponential-in-$v$ scan only when that many bits were supplied. Hence its running time is polynomial in the proof length, as required, and it is a surjection onto tautologies.

Let $\tau_n=\bigwedge_{i=1}^n(x_i\vee\neg x_i)$, choosing $n$ so that this formula is not the default $\tau_0$. Its formula length is $O(n\log(n+2))$, but every $T$-proof has at least $2^n$ table entries. Now extend $T$ with a tagged input containing any formula of the syntactic form $\tau_n$, which is output immediately. Recognition and output take polynomial time, and every added output is a tautology. The resulting system is still sound and surjective, and the same family has proofs of length $O(n\log(n+2))$. Thus a proved exponential lower bound for a particular system and family can coexist with short proofs in another permitted system. This is an illustrative construction, not a claim that any familiar strong system simulates all others.

Verification and first remaining gap.

The companion checks enumerate all normalized clauses on up to six variables, confirm that every non-tautological clause valid on even parity has full width, and count exactly $2^{n-1}$ necessary excluded odd assignments. They test all eight XOR triples and the four displayed gate clauses. They also enumerate all $2\times3$ affine systems, comparing the existence of a solution with the absence of a certificate (a13:dual). These checks support the finite identities, while the proofs cover arbitrary sizes.

The first missing lemma for the proposed upper-bound route is a sound, complete polynomial-time verifier whose certificates for all unsatisfiable Boolean gate systems have length polynomial in the original encoding. The affine lemma proves this only for a tractable subclass. For a lower-bound route, the missing quantifier is a bound against every Cook--Reckhow system, including systems with additional certificate types. Next work must address nonlinear constraints, retained auxiliary variables, and this universal quantifier together; more accurate parity clause counts will not bridge the gap.

Outcome.

UNRESOLVED. The attempt proves an exact parity representation bound, constructs polynomial certificates for an affine contradiction family, and exhibits a proof-system extension defeating a particular exponential lower bound. These elementary results are presented without novelty claims. They identify two invalid inferences, but establish neither $\mathsf{NP}=\mathsf{coNP}$ nor $\mathsf{NP}\ne\mathsf{coNP}$.

Sources

• S1 Scott Aaronson, "P =? NP," in Open Problems in Mathematics (J. F. Nash Jr., M. Th. Rassias, eds.), Springer, 2016, pp. 1-122. https://www.scottaaronson.com/papers/pnp.pdf. Formulation source.
• S2 Proof Complexity and Feasible Interpolation — Amirhossein Akbar Tabatabai $2025$. https://arxiv.org/html/2505.03002v1. Further reference; not a proof endorsement.
• S3 Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size — de Rezende, Engström, Ghannane and Risse $2026$. https://eccc.weizmann.ac.il/report/2026/078/. Further reference; not a proof endorsement.
• S4 Simulating Polynomial-Time Nondeterministic Turing Machines via Nondeterministic Turing Machines — Tianrong Lin, v28. https://arxiv.org/abs/2406.10476. Further reference; not a proof endorsement.
• S5 A Critique of Lin's On NP versus coNP and Frege Systems — DeJesse, Lyudovyk, Pai and Reidy $2025$. https://arxiv.org/abs/2505.05658. Further reference; not a proof endorsement.
• S6 Proofs of NP = coNP = PSPACE: Current upgrade — Lev Gordeev and Edward Hermann Haeusler, v3. https://arxiv.org/abs/2311.17939. Further reference; not a proof endorsement.
• S7 A simplified lower bound for implicational logic — Emil Jeřábek (September 2024 version; published 2025). https://arxiv.org/html/2303.15090v3. Further reference; not a proof endorsement.
• E1 Stephen A. Cook and Robert A. Reckhow, The Relative Efficiency of Propositional Proof Systems, Journal of Symbolic Logic 44$1$ $1979$, pp. 36--50, especially Propositions 1.1 and 1.4 and Definition 1.3. https://www.cs.toronto.edu/~sacook/homepage/cook_reckhow.pdf. https://doi.org/10.2307/2273702. Primary source for the proof-system equivalence and definition; consulted 27 September 2026.

NP versus coNP Problem

Definitions and mathematical statement

For $L\subseteq\{0,1\}^*$ write $\overline L=\{0,1\}^*\setminus L$ and set $\mathsf{coNP}=\{\overline L:L\in\mathsf{NP}\}$. The question is $\mathsf{NP}=\mathsf{coNP}$. A Cook--Reckhow proof system is a polynomial-time computable surjection $P:\{0,1\}^*\to\mathsf{TAUT}$, where $\mathsf{TAUT}$ is the set of propositional tautologies. Polynomial boundedness means \[ \exists\text{ polynomial }q\ \forall\varphi\in\mathsf{TAUT}\ \exists\pi: P(\pi)=\varphi,\quad|\pi|\le q(|\varphi|). \] The equivalent proof-system question permits choosing the system; it is not restricted to a familiar calculus.

Formulation and concept references: [S1].

Short English statement

Does efficient certification of yes-answers always come with efficient certification of no-answers?

Research attempt

Current frontier.

Research check: 27 September 2026. The Cook--Reckhow equivalence concerns the existence of some polynomially bounded proof system; its exact quantifiers and the notion of simulation are reviewed in Krajicek, Theorem 1.2 and Section 2. [E1]. Feasible interpolation and the 2026 bounded-line, tree-like semantic lower bounds concern specified proof-system models. [S2], [S3]. The critique of Lin identifies an error in the particular construction it examines; it is not itself a separation of $\mathsf{NP}$ from $\mathsf{coNP}$, and is not treated here as an audit of every later revision. [S5]. The attempt below asks whether an elementary algebraic refutation can supply short certificates without hiding the original verification task.

Attack route.

An algebraic certificate could prove unsatisfiability, a combinatorial proof-system lower bound could disprove polynomial boundedness of a particular calculus, and diagonalization might try to defeat every calculus. The first requires efficiently checkable identities; the second needs a universality argument; the third needs a polynomially verifiable language after diagonalization. We pursue the first route and then use an explicit proof-system construction to stress-test the second.

Attempt: a surprisingly short formal refutation.

Work in the Boolean ring \[ R_n={\mathbb{F}}_2[x_1,\ldots,x_n]/(x_1^2-x_1,\ldots,x_n^2-x_n). \] Every element has a unique multilinear representative and is determined by its values on $\{0,1\}^n$. For a CNF formula with clauses $C_1,\ldots,C_m$, let $f_j$ be the product of the false-literal indicators in clause $j$: a positive literal $x_i$ contributes $1+x_i$, and a negative literal $\neg x_i$ contributes $x_i$. Thus $f_j(a)=1$ exactly when $a$ falsifies $C_j$.

In any commutative ring of characteristic two, telescoping gives \[ \sum_{j=1}^m f_j\prod_{i<j}(1+f_i) =1+\prod_{j=1}^m(1+f_j). \tag{13.1} \] For example, the difference between two consecutive prefix products is $f_j\prod_{i<j}(1+f_i)$; summing cancels the intermediate products. The product on the right is the truth function of the entire CNF. Consequently the formula is unsatisfiable if and only if \[ \sum_{j=1}^m g_j f_j=1\ \hbox{in }R_n, \qquad g_j=\prod_{i<j}(1+f_i). \tag{13.2} \] All the $g_j$ have small arithmetic circuits, constructed using shared prefix products; even without sharing, their total circuit size is polynomial in the formula length. This is an exact identity criterion, not an unproved existence claim about coefficients.

The apparent proof of $\mathsf{NP}=\mathsf{coNP}$ breaks at verification. Checking $13.2$ as an equality of Boolean functions is precisely the unsatisfiability question for these explicitly constructed circuits. Ordinary formal polynomial identity testing does not test equality in $R_n$. For the inconsistent clauses $x$ and $\neg x$ one has $f_1=1+x$, $f_2=x$, $g_1=1$, $g_2=x$, so the left side is $1+x+x^2$. It equals $1$ in $R_1$, but not in ${\mathbb{F}}_2[x]$.

One could instead seek an ordinary polynomial identity \[ \sum_j g_jf_j-1=\sum_{i=1}^n h_i(x)(x_i^2-x_i). \tag{13.3} \] The left side vanishes on the Boolean cube for an unsatisfiable formula, so such polynomials $h_i$ exist: successively reduce powers of each variable modulo $x_i^2-x_i$ and retain the quotients. However, this procedure on expanded polynomials can be exponentially large. Neither small circuits for every required $h_i$ nor a deterministic polynomial-time verification procedure for the chosen compressed identity format has been established. The role of representation and proof checking here is consistent with the proof-complexity distinctions in [S2]; $13.1$--$13.3$ are the explicit calculations of this attempt.

Attempt: why random Boolean testing is insufficient.

For $a\in\{0,1\}^n$ put \[ \delta_a(x)=\prod_{i:a_i=1}x_i\prod_{i:a_i=0}(1+x_i). \] This has a linear-size circuit and degree $n$, and is nonzero at exactly one Boolean input. A test of $\delta_a=0$ using $T$ independent uniform Boolean samples accepts the false identity with probability $(1-2^{-n})^T\geq1-T2^{-n}$. Thus polynomially many such tests cannot supply the required sound certificate. This is not a contradiction to formal polynomial testing over large extension fields: the intended equality here is an equality of Boolean functions, with a different domain and quotient. Even bounded-error checking would not automatically be a deterministic Cook--Reckhow verifier.

Attempt: a family can be made easy by changing the system.

Let $\tau_n$ be any uniformly polynomial-time computable family of tautologies, with output length bounded by a polynomial in $n$ and at least $n$. There exists a Cook--Reckhow system giving $\tau_n$ proofs of length $O(n)$. Define a machine on strings with two disjoint tags. On a correctly formatted string $0\,1^n$, output $\tau_n$. On a string encoding $1$, a formula $\varphi$, and at least $2^{v(\varphi)}$ padding symbols, enumerate all assignments and output $\varphi$ if it is a tautology. In every other case output the fixed tautology $p\lor\neg p$. Here $v(\varphi)$ is its number of distinct variables, after relabeling them consecutively.

Parsing the padding bound and evaluating all assignments take time polynomial in the proof length. Every output is a tautology, every tautology has a sufficiently padded proof, and $\tau_n$ has the special short proof. Therefore this is a polynomial-time surjection onto $\mathsf{TAUT}$. The usual definition requires surjectivity, not a uniform short-proof bound for every tautology. [E1]. The construction does not make all tautologies easy. It shows why a lower bound for one explicit family in one fixed calculus cannot, on its own, exclude polynomial boundedness of every calculus.

Stress test.

The characteristic-two signs in $13.1$ are essential; they were not silently used over ${\mathbb{Q}}$. Empty clauses, tautological clauses, and repeated literals are handled by their Boolean indicators; the empty conjunction is satisfiable and yields a zero left side rather than a refutation. The construction of a special proof system assumes the supplied family really consists of tautologies. It is a mathematical construction for a sound family, not an algorithm deciding whether an arbitrary generator has that property. Finally, exponential padding in the fallback branch is permitted because verification is polynomial in proof length; it does not meet the missing polynomial boundedness in formula length.

Outcome.

Outcome: Exploratory approach with unresolved gap. The explicit telescoping certificate exposes a verification bottleneck: short coefficient circuits are available, but the required Boolean-ring identity check is not thereby efficient. A small point-indicator gives a sharp obstruction to naive randomized checking. The tailored-system construction explains a separate quantifier obstacle to extrapolating restricted proof lower bounds. No proof system polynomially bounded on all tautologies, or separation excluding every such system, has been obtained. Historical novelty of these observations is not asserted.

Sources

• S1 Scott Aaronson, "P =? NP," in Open Problems in Mathematics (J. F. Nash Jr., M. Th. Rassias, eds.), Springer, 2016, pp. 1-122. https://www.scottaaronson.com/papers/pnp.pdf. Catalogue formulation source.
• S2 Proof Complexity and Feasible Interpolation — Amirhossein Akbar Tabatabai $2025$. https://arxiv.org/html/2505.03002v1. Catalogue research/status reference; not a proof endorsement.
• S3 Superpolynomial Length Lower Bounds for Tree-Like Semantic Proof Systems with Bounded Line Size — de Rezende, Engström, Ghannane and Risse $2026$. https://eccc.weizmann.ac.il/report/2026/078/. Catalogue research/status reference; not a proof endorsement.
• S4 Simulating Polynomial-Time Nondeterministic Turing Machines via Nondeterministic Turing Machines — Tianrong Lin, v28. https://arxiv.org/abs/2406.10476. Catalogue research/status reference; not a proof endorsement.
• S5 A Critique of Lin's On NP versus coNP and Frege Systems — DeJesse, Lyudovyk, Pai and Reidy $2025$. https://arxiv.org/abs/2505.05658. Catalogue research/status reference; not a proof endorsement.
• S6 Proofs of NP = coNP = PSPACE: Current upgrade — Lev Gordeev and Edward Hermann Haeusler, v3. https://arxiv.org/abs/2311.17939. Catalogue research/status reference; not a proof endorsement.
• S7 A simplified lower bound for implicational logic — Emil Jeřábek (September 2024 version; published 2025). https://arxiv.org/html/2303.15090v3. Catalogue research/status reference; not a proof endorsement.
• E1 Jan Krajíček, The Cook-Reckhow definition, arXiv:1909.03691v1 $2019$, Theorem 1.2 and Section 2. https://arxiv.org/html/1909.03691v1. Added research source. Proof-system definition, polynomial boundedness and simulation. Consulted 27 September 2026.