Episode 141, October 2026

Real solutions at level 26?

A claim that the existential theory of the reals, and existential–universal real sentences with circuit-given polynomials, sit at a fixed level of the counting hierarchy

Covers result 141 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.

Play Episode 141: Real solutions at level 26? A circle with one marked point above a tower of 26 majority-voting layers inside PSPACE.

5:56. English captions available. The video loads from YouTube when you press play.

Chapters

The claim, in plain words

Given polynomial equations and inequalities with integer coefficients, is there a real point that satisfies them all? On the unit circle x² + y² = 1 there is a point with xy > 1/4, but none with xy > 1/2: the hyperbola xy = 1/2 only touches the circle. Deciding such questions is the existential theory of the reals (ETR); the problems that reduce to it in polynomial time form the class ∃ℝ, which captures many geometric realization and continuous feasibility problems. As the paper cites the history, Tarski showed these questions are decidable, Collins gave cylindrical algebraic decomposition, Canny placed the existential fragment in polynomial space, and Renegar did the same for any fixed number of quantifier blocks.

The counting hierarchy lies inside polynomial space. Its first level, PP, decides by a majority vote over a fast machine’s random choices; each next level gives such a machine an oracle for the level below. Allender, Bürgisser, Kjeldgaard-Pedersen and Miltersen showed that the sign of an integer computed by a division-free arithmetic circuit can be decided in this hierarchy, even though such integers can have far too many bits to write down.

Result 141 is one OpenAI preprint (35 pages, October 4, 2026). Theorem 1.1 claims an absolute level j such that the true sentences ∃x ∈ ℝ^r ∀y ∈ ℝ^s : Φ(x, y) form a language in C_jP, where Φ combines atoms p = 0 and p > 0 with AND, OR and NOT, and each p is given by an arithmetic circuit (+, −, ×) with binary integer constants. The level does not depend on the input, the numbers of variables, the degrees or the coefficient sizes. For the purely existential part, Theorem A.1 counts the levels: ETR ∈ C₂₆P, and so ∃ℝ ⊆ C₂₆P.

What it doesn’t claim

A faster algorithm: this is a containment. It is not known whether the counting hierarchy is smaller than polynomial space, so the result does not show these problems are easier than PSPACE-complete ones. The level j for two quantifier blocks is not computed, the paper calls 26 a conservative bound, and three or more blocks are not covered. The paper does not present membership in the counting hierarchy as a known open problem. It builds on the counting arithmetic of Allender and coauthors, and cites recent work placing Hilbert’s Nullstellensatz over the rationals (Andrews, Garg and Schost) and approximate polynomial satisfiability (Balaji, Shirmohammadi, Tavenas and Worrell) in the counting hierarchy; over the reals, it says, one must also control whether solutions are real and attained.

Where it stands

Posted as a preprint: OpenAI, 35 pages, dated October 4, 2026
Peer reviewed: Not yet
Checked in Lean: No

Last checked October 19, 2026. The preprint has not been revised. It is not formalized in Lean, and we found no Lean files for this result in the repository. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

One quartic. Give every circuit wire its own variable, so every condition becomes an equation of degree at most two. The sum of their squares is one nonnegative quartic F, with a real zero exactly when the existential sentence is true.
A penalty minimum. Add a coercive bowl G to u times F and minimize. If F has a real zero the minimum stays bounded as u grows; otherwise it runs off to infinity.
Eigenvalues and one large value. Values at critical points are eigenvalues of multiplication by the function on the critical-point equations, a matrix of dimension 5ⁿ, far too big to write down. The limit in u is replaced by one specialization u = 2^σ, with σ given by an explicit formula: F has a real zero exactly when a resulting one-variable polynomial has a real root below a fixed cutoff 2^ρ.
Counting instead of computing. Everything is handled implicitly: counting is majority voting, products modulo a prime become sums of discrete logarithms, coefficients come from averages over a finite field, and determinants come from traces, without building matrices.
Signs of gigantic integers. A short list of derivative signs names one real root, and is turned into a polynomial test: a suitable root exists exactly when, for some guessed test list and small shift, a determinant is negative. The sign of that integer is recovered from small residues, by approximating it divided by a product of primes, modulo one, and doubling until the result lands well away from zero.
The for-all block. A further geometric argument (a growth test, degree pieces, candidate coordinates from roots of computed polynomials) finds a good parameter without describing the whole good set.

The numbers in the video

2^2⁶⁴ mod 1,000,003 = 560,597 by 64 modular squarings. The circuit (a+1)² − a² − 2a with a = 2⁶⁴ has exact value 1 but evaluates to about −3.69 × 10¹⁹ in double precision.
For h_u = x⁶ + 6uF in one variable: with F = (x² − 2)² the minimum is 4.862, 7.454, 7.941, 7.994, 7.9994 and 7.99999 at u = 1, 10, …, 10⁶, tending to 8; with F = (x² + 1)² it is exactly 6u.
The specialization in one variable, using the paper’s G and formulas fed the exact coefficient size H = 142: ρ = 146 and σ = 2,456; the resulting polynomial has degree 5 and coefficients of up to 17,264 bits; 2 of its 3 real roots lie below the cutoff in the true case, and its 1 real root does not in the false case. The paper’s a-priori bound would give a much larger u.
A toy multiplication map of dimension 9 with one real eigenvalue, 4.9088, and four complex pairs: det(M − cI) is positive for c = 3, 4 and 4.9 and negative for c = 4.95, 5 and 6.
Signs from residues at toy scale: 84 primes between 100 and 600 (a 692-bit product) recover the signs of 2⁶⁴ − 3⁴⁰, 3⁴¹ − 2⁶⁵, 1 and 0.

Read the source

Existential–universal real sentences in the counting hierarchy (PDF), 35 pages.
The collection’s catalog, where this is result 141.

The paper

OpenAI groups related papers into one result; this one has a single paper.

Existential–universal real sentences in the counting hierarchy

Transcript

Read the full script

0:00Is there a real solution?

Given some polynomial equations and inequalities with integer coefficients, is there any real point that satisfies them all? For example, is there a point on the unit circle where x times y exceeds 1/4? Yes. Where it exceeds 1/2? No. This is the existential theory of the reals. Problems that reduce to it in polynomial time form a class called ∃R, which captures many geometric realization and continuous feasibility problems. Tarski showed such questions are decidable, Collins gave cylindrical algebraic decomposition, and Canny placed the existential fragment in polynomial space; Renegar’s bounds do the same for any fixed number of quantifier blocks. The counting hierarchy sits inside polynomial space. Its first level, PP, is decision by a majority vote over a fast machine’s random choices, and each next level gives such a machine an oracle for the level below. Allender, Bürgisser, Kjeldgaard-Pedersen and Miltersen showed that deciding the sign of an integer computed by a division-free arithmetic circuit lies in this hierarchy. That is subtle: n squarings of two produce 2^(2^n), and after a few hundred of them that number has more bits than could ever be written down, although its remainder modulo a prime is easy. Ordinary floating point gets such signs wrong: in our check, a circuit whose exact value is one evaluates to about −37 quintillion in double precision.

1:33The claim

Result 141 is a single OpenAI preprint, 35 pages, dated October 4. It claims that sentences of the form, there exist real x such that for all real y, a formula holds, can be decided at one fixed level of the counting hierarchy, even when the polynomials are given as arithmetic circuits with binary integer constants. For the purely existential part, it counts the levels: the existential theory of the reals, and so all of ∃R, lies at level 26. That is a tower of 26 nested layers of majority voting, still inside polynomial space. This is a containment, not a faster algorithm. It is not known whether the counting hierarchy is smaller than polynomial space, so the result does not show these problems are easier than PSPACE-complete ones. The level for the two-block sentences is not computed, 26 is called conservative, and three or more blocks are not covered. Nor does the paper present membership in the counting hierarchy as a known open problem. It builds on the counting arithmetic of Allender and coauthors, and cites recent work placing Hilbert’s Nullstellensatz over the rationals, and approximate polynomial satisfiability, in the counting hierarchy; over the reals, it says, one must also control whether solutions are real and attained. There is no Lean formalization.

3:01How the proof goes

For the existential part, the proof goes like this. Give every circuit wire its own variable, so every condition becomes an equation of degree at most two; the sum of their squares is one nonnegative quartic, which has a real zero exactly when the sentence is true. Then add a coercive bowl to u times that quartic, and minimize. If the quartic has a real zero, the minimum stays bounded as u grows; if not, it runs off to infinity. In our one-variable check, for x² = 2, the minimum tends to 8; for x² = −1, it is exactly 6u. Minimum values are eigenvalues: the critical-point equations turn multiplication by the function into a matrix, of dimension five to the power of the number of variables, far too big to write down. The limit in u is replaced by one astronomically large value. In our one-variable run, the paper’s formula, fed the exact coefficient size, takes u equal to 2^2456, and the resulting polynomial has coefficients of up to about 17,000 bits; it has a real root below a fixed cutoff exactly in the true case. Everything is computed implicitly: counting is majority voting, products modulo a prime become sums of discrete logarithms, and determinants come from traces, without building matrices. To pick out one real root, the paper uses a short list of derivative signs there, turned into a polynomial test, and the question collapses to signs of gigantic integers: a suitable real root exists exactly when, for some guessed test and small shift, a determinant comes out negative. In our toy, such a determinant changes sign exactly when the test value passes the one real eigenvalue, while complex pairs contribute positive factors. The integer’s sign is recovered from small residues: approximate it divided by a product of primes, modulo one, and keep doubling until it lands far from zero. The for-all block needs a further geometric argument, which finds a good parameter through roots of computed polynomials, without describing the whole good set.

5:15Where it stands

The preprint is not peer reviewed and has not been revised. It is not formalized in Lean, and we found no Lean files for this result in the repository. It is not among those OSVerify reviewed, and we have seen no expert review. If it holds, deciding whether polynomial systems have real solutions, even with arithmetic circuits and one block of for-all quantifiers, sits at a fixed level of the counting hierarchy, a refinement of the polynomial-space bounds of Canny and Renegar. Whether that level is truly smaller than polynomial space remains unknown.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.