gpt 6 astra pro attempt on CS-3

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.