NP versus the Existential Theory of the Reals

NP versus the Existential Theory of the Reals

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 141; 2026-10-04), the asserted result is that existential real feasibility, and more generally existential--universal real sentences with circuit-given integer polynomials, lie in a fixed counting-hierarchy level.

Mathematical statement of the claimed result

Manuscript 1.

Let $\mathcal T_{\exists\forall}$ consist of true real sentences \[ \exists x\in\mathbb R^r\ \forall y\in\mathbb R^s:\Phi(x,y), \] where $r,s\ge0$, $\Phi$ is an explicitly encoded Boolean combination of $p=0$ and $p>0$, and each $p$ is an acyclic arithmetic circuit with binary integer constants and $+,-,\times$ gates, with no division or exponentiation gates. Malformed encodings are rejected. Define $\mathsf C_0=\mathrm P$, $\mathsf C_{j+1}=\bigcup_{A\in\mathsf C_j}\mathrm{PP}^A$. The claim is \[ \exists j\in\mathbb N:\quad\mathcal T_{\exists\forall}\in\mathsf C_j, \] with one absolute level independent of input size, variable counts, degrees and coefficient sizes. These are uniform bit-time complexity classes.

Outline of the argument

For manuscript 1 (family 141; 2026-10-04), critical-point deformation turns quantified fibers into short algebraic witnesses. Modular evaluation accesses huge controlled polynomials without expansion, while residue--trace determinant formulas and compressed derivative-sign labels recover the needed root signs inside the counting hierarchy.

Formal verification

No Lean formalization is listed at this snapshot for manuscript 1 (family 141; 2026-10-04).

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, Existential–universal real sentences in the counting hierarchy, 2026-10-04; citation key OAI:Existential-universal-real-sentences-in-the-counting-hierarchy-October-4-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• OpenAI catalogue entry.

NP versus the Existential Theory of the Reals

Definitions and mathematical statement

The existential theory of the reals asks whether a sentence $\exists x_1,\ldots,x_m\in{\mathbb{R}}\;\Phi(x_1,\ldots,x_m)$ is true, where $\Phi$ is a quantifier-free Boolean combination of polynomial equalities and inequalities with integer coefficients given in finite binary encoding. The complexity class $\exists{\mathbb{R}}$ consists of languages polynomial-time many-one reducible to this decision problem. With $\mathrm{NP}$ defined by polynomial-length binary certificates and polynomial-time deterministic verification, the selected question is \[ \exists{\mathbb{R}}\subseteq\mathrm{NP},\qquad\text{equivalently }\mathrm{NP}=\exists{\mathbb{R}}. \] Witnesses for the real formula itself need not be rational or have short numerical encodings; the question concerns existence of some NP verification scheme, not merely writing down a real solution.

Formulation and concept references: [S1].

Short English statement

Can the existence of solutions to finite systems of real polynomial constraints always be certified by a short binary proof that is efficiently checkable?

Research attempt

Current frontier.

The established inclusions are $\mathrm{NP}\subseteq\exists{\mathbb{R}}\subseteq\mathrm{PSPACE}$. The compendium emphasizes both the absence of a general short-certificate theorem and the fact that large coordinate descriptions do not themselves separate these classes [S1], Sections 1.2--1.3. A useful adjacent problem is

\textsf{PosSLP}

: deciding positivity of an integer represented by a straight-line arithmetic program. Allender--Bürgisser--Kjeldgaard-Pedersen-- Miltersen place it in the counting hierarchy, but that is not an NP bound [E1]. No verified 2024--2026 result located for this entry settles the selected equality. The attempt below constructs a genuine binary certificate for a quantitative subclass and tests the proposed extensions.

Attack route.

Literal rational solutions fail when only irrational solutions exist, and even strictly feasible rational solutions can require exponentially many bits. Algebraic towers can be short, but efficient general sign checking is an additional problem. A third route is to certify a solution indirectly by a rational contraction box. Its prospective advantage is that no exact encoding of the solution is needed. Its missing input is a polynomial-size covering theorem: every satisfiable instance would need a short certificate of this kind, or a controlled generalization covering singular and poorly conditioned solutions.

Attempt: reducing representation issues without hiding cost.

Introducing one variable for each arithmetic gate replaces polynomial computations by quadratic gate equations. Binary-encoded exponents can be evaluated by repeated squaring with a number of gates polynomial in their bit lengths. A guessed consistent truth assignment to the Boolean combination selects sign conditions on the computed outputs. This explains why quadratic systems are a useful test class; it does not manufacture short values for the added real variables. In particular, the computation model throughout this entry is ordinary binary computation, not unit-cost arithmetic on arbitrary real or exponentially long integer registers.

For the positive lemma, consider the explicit subclass \begin{equation}\label{wsref-0-65-71-31-35-38-2d-73-79-73-74-65-6d} P_1(x)=\cdots=P_m(x)=0,\qquad Q_j(x)>0\quad(1\le j\le s), \qquad x\in{\mathbb{R}}^m, \end{equation} where all $P_i,Q_j$ are rational polynomials of degree at most two, given by their coefficients. Clearing positive denominators gives an instance of the target problem. The equal number of equations and variables is a hypothesis for this lemma, not a normal form asserted for every instance.

Attempt: a rational geometric certificate.

A certificate consists of $x_0\in{\mathbb{Q}}^m$, $r\in{\mathbb{Q}}_{>0}$, and an invertible matrix $A\in M_m({\mathbb{Q}})$. Let \[ B=\{x:\|x-x_0\|_\infty\le r\},\qquad P=(P_1,\ldots,P_m)^t, \qquad H_k=\partial_kDP. \] The matrices $H_k$ are constant because $P$ is quadratic. All matrix norms in the next display are induced $\ell^\infty$ norms. Compute the rational numbers \begin{align} q&=\|I-A DP(x_0)\|_\infty+ r\sum_{k=1}^m\|A H_k\|_\infty,\label{wsref-0-65-71-31-35-38-2d-71}\\ M_j&=\|DQ_j(x_0)\|_1+ r\sum_{k=1}^m\|\partial_k DQ_j\|_1.\label{wsref-0-65-71-31-35-38-2d-4d} \end{align} The verifier checks, by exact rational arithmetic, \begin{equation}\label{wsref-0-65-71-31-35-38-2d-63-68-65-63-6b-73} \det A\ne0,\quad q\le\tfrac12,\quad \|A P(x_0)\|_\infty\le r/2,\quad Q_j(x_0)-rM_j>0\ (1\le j\le s). \end{equation}

Certificate lemma. Every accepted certificate proves that (eq158-system) is satisfiable. Verification takes time polynomial in the combined binary length of the instance and certificate.

Proof of soundness. Put $T(x)=x-A P(x)$. For $x\in B$, \[ DP(x)=DP(x_0)+\sum_k(x_k-x_{0,k})H_k, \qquad\|DT(x)\|_\infty\le q. \] The segment between any two points of $B$ lies in $B$, so the mean value formula proves that $T$ is $q$-Lipschitz on $B$. Also \[ \|T(x)-x_0\|_\infty \le\|AP(x_0)\|_\infty+q\|x-x_0\|_\infty\le r. \] Thus $T$ maps the complete closed box to itself and is a contraction. Successive iteration is Cauchy because successive differences decrease geometrically; its limit $x_*$ satisfies $T(x_*)=x_*$. Since $A$ is invertible, $P(x_*)=0$. Equation (eq158-M) bounds $\sup_{x\in B}\|DQ_j(x)\|_1$, so \[ Q_j(x_*)\ge Q_j(x_0)-rM_j>0. \] This proves all the required conditions. There is no need to compute the limit, approximate its coordinates to an unbounded precision, or test a real number for exact equality.

Proof of verification complexity. Polynomial evaluation at rational points of supplied bit length, rational matrix multiplication, row sums of absolute values, and rational comparisons require polynomially many integer operations on polynomial-bit integers here. Exact determinant computation also has polynomial bit complexity, for example by fraction-free elimination. The finite sums contain only polynomially many terms. Hence the verification bound is polynomial in the supplied encoding length. This statement alone does not bound that length by a polynomial in the original instance. $\square$

An irrational solution is not an obstacle to this certificate. For $P(x)=x^2-2$ and $Q(x)=x$, take \[ x_0=\tfrac32,\qquad r=\tfrac14,\qquad A=\tfrac13. \] Then $q=1/6$, $|AP(x_0)|=1/12<r/2$, and $Q(x_0)-rM=5/4>0$. The certificate proves existence of the positive root without encoding $\sqrt2$ as a binary number. These inequalities are also checked in the accompanying exact-arithmetic script.

Attempt: when polynomial-length boxes do follow.

Here is a quantitative subclass for which the preceding verifier really does give short certificates. Let $N$ be the instance length and suppose there is a feasible $x_*$ with invertible $DP(x_*)$, and a fixed polynomial $h$ such that \begin{equation}\label{wsref-0-65-71-31-35-38-2d-63-6f-6e-64-69-74-69-6f-6e} \|x_*\|_\infty,\ \|DP(x_*)^{-1}\|_\infty\le2^{h(N)}, \qquad \min_j Q_j(x_*)\ge2^{-h(N)}. \end{equation} For $s=0$ omit the minimum condition. The quadratic coefficients and the number of variables have bounds of the same single-exponential type from the input encoding. On a unit neighborhood of $x_*$ all first and second derivatives are therefore bounded by $2^{g(N)}$ for a fixed polynomial $g$, after increasing $g$ as necessary.

Choose a dyadic radius $r=2^{-k(N)}$ sufficiently small that the Hessian contribution in (eq158-q), evaluated with $A_*=DP(x_*)^{-1}$, is at most $1/8$, and that all inequalities retain a margin on the radius-$2r$ box. Approximate $x_*$ and $A_*$ by dyadic $x_0,A$ to an accuracy $2^{-l(N)}$, with $l$ another sufficiently large fixed polynomial. The derivative bounds and the bounds on $A_*$ imply \[ \|I-A DP(x_0)\|_\infty\le\tfrac18,\qquad \|A P(x_0)\|_\infty\le r/2, \] and keep the inequalities in (eq158-checks) strict. For example, choose the rounding errors smaller than $r$ times the reciprocal of a suitable product of the finitely many bounds $2^{g(N)}$. Such a choice still has polynomial bit length. Finally $\|I-A DP(x_0)\|<1$ implies that $A DP(x_0)$, and hence the square matrix $A$, is invertible. This constructs a polynomial-length certificate under (eq158-condition).

No claim is made that every feasible system has such a point. Singular solutions, positive-dimensional solution sets, or very small inequality margins require another argument. Converting them to the square regular case by slicing or deflation without uncontrolled growth is itself a missing lemma.

Stress test: small coordinates even in a bounded open set.

Consider the strictly feasible quadratic system \begin{equation}\label{wsref-0-65-71-31-35-38-2d-73-6d-61-6c-6c} 0<x_0<\tfrac12,\qquad 0<x_{i+1}<x_i^2\quad(0\le i<n). \end{equation} All coordinates lie in $(0,1)$, but induction gives $0<x_n<2^{-2^n}$. If $x_n=a/b$ is a reduced positive rational, then $a\ge1$ and $b>2^{2^n}$, so its ordinary denominator encoding has more than $2^n$ bits. Boundedness and strict feasibility do not imply a polynomial-length literal rational witness.

Nevertheless this family has a short description of a witness: $x_0=1/4$ and $x_{i+1}=x_i^2/2$, equivalently $x_i=2^{-(3\cdot2^i-1)}$. The recurrence proves all constraints. Therefore (eq158-small) is not a complexity separation; it only refutes a particular coordinate-encoding proposal.

A different obstruction affects a single primitive algebraic-number encoding. The system \[ y_0^2=2,\quad y_0>0,\qquad y_{i+1}^2=y_i,\quad y_{i+1}>0 \quad(0\le i<n) \] has all coordinates in $(1,2)$, yet $y_n$ has degree $2^{n+1}$ over ${\mathbb{Q}}$. Indeed its minimal polynomial is $T^{2^{n+1}}-2$, irreducible by Eisenstein at $2$. A tower description is short. In fact such systems may also be amenable to geometric certificates; exponential algebraic degree is not a proof that all certificate systems are long.

Stress test: the price of arithmetic compression.

Let an integer straight-line program start from $1$ and use addition, subtraction, and multiplication. Introduce one real variable per gate and impose its defining equation, such as $z_k-z_i z_j=0$, together with the initial constant equation and $z_{\mathrm{out}}>0$. Induction on the gates shows that this polynomial-size existential formula is satisfiable exactly when the program's integer output is positive. Thus \begin{equation}\label{wsref-0-65-71-31-35-38-2d-70-6f-73-73-6c-70} \mathrm{NP}=\exists{\mathbb{R}}\quad\Longrightarrow\quad \textsf{PosSLP}\in\mathrm{NP}. \end{equation} For integer output $z$, the complement condition $z\le0$ is equivalent to $1-z>0$, obtained by two extra gates. Hence the same implication would actually put $\textsf{PosSLP}$ in $\mathrm{NP}\cap\mathrm{coNP}$. The reduction is proved here; the role of this sign problem in numerical complexity is established in [E1] and discussed in [S1].

Consequently a proposed universal certificate consisting of succinct arithmetic programs cannot simply declare their signs efficiently checkable. Exact cancellation may involve integers with exponentially many bits. Such a declaration assumes a major part of the problem rather than solving it. Conversely, the two explicit large-description families above do not show $\textsf{PosSLP}\notin\mathrm{NP}$ or $\mathrm{NP}\ne\exists{\mathbb{R}}$. Nor does (eq158-posslp) imply $\mathrm P=\mathrm{NP}$; the latter is a different, stronger algorithmic assertion. Positivstellensatz certificates of infeasibility address the opposite side and do not by themselves provide the required satisfiability certificates.

Outcome.

Outcome: Exploratory approach with unresolved gap.

The attempt supplies a sound polynomial-time binary verifier for rational contraction certificates, proves polynomial certificate length under explicit regularity and margin bounds, and gives exact small examples. It also proves why two naive witness-size arguments fail, and identifies a precise compressed-sign consequence of the full target. No novelty is claimed for the underlying contraction principle or the standard straight-line-program reduction.

What remains missing is a universal polynomial-size certificate theorem, including singular feasible sets and arbitrarily ill-conditioned or narrow solution regions, without assuming polynomial-time succinct sign arithmetic. The large-coordinate and large-degree constructions only rule out specified formats; they do not rule out NP verification in general. Thus neither equality nor separation of the two classes has been proved.

Sources

• S1 M. Schaefer, J. Cardinal, T. Miltzow, The Existential Theory of the Reals as a Complexity Class: A Compendium, arXiv:2407.18006, 2024. https://arxiv.org/abs/2407.18006. Catalogue formulation source.
• E1 Eric Allender, Peter Bürgisser, Johan Kjeldgaard-Pedersen, and Peter Bro Miltersen, On the Complexity of Numerical Analysis, SIAM Journal on Computing 38$5$ $2009$, 1987--2006, Introduction and the PosSLP counting-hierarchy theorem. https://doi.org/10.1137/070697926. Author manuscript: https://www.cs.rutgers.edu/~allender/papers/slp.pdf. Consulted 27 September 2026; a counting-hierarchy bound is not treated as membership in NP.