The existential theory of the reals in the counting hierarchy
The existential theory of the reals in the counting hierarchy concerns the complexity of deciding whether a system of polynomial constraints with integer coefficients has a real solution (the problem ETR, with complexity class ∃ℝ). ETR is NP-hard and, by Canny's theorem, decidable in polynomial space. Whether it lies in the counting hierarchy CH, a hierarchy of complexity classes built from probabilistic polynomial time and contained in PSPACE, is the question addressed here. A manuscript dated 4 October 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims that it does. A parallel claim with a stronger bound appeared on arXiv on 7 October 2026. This page summarizes the published claims and lists related public work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the manuscript's introduction: Tarski proved the decidability of the first-order theory of real closed fields, Collins introduced cylindrical algebraic decomposition, Canny placed the existential fragment in PSPACE, and Renegar's bounds give polynomial space for each fixed number of quantifier blocks. Allender, Bürgisser, Kjeldgaard-Pedersen and Miltersen showed that PosSLP, the positivity of the integer output of a division-free straight-line program, lies in CH.
- Two recent counting-hierarchy results on polynomial feasibility are cited by the manuscript. Andrews, Garg and Schost (arXiv:2602.17904) place Hilbert's Nullstellensatz in CH. Balaji, Shirmohammadi, Tavenas and Worrell (arXiv:2610.00644, September 2026) place approximate polynomial satisfiability in CH. Both concern solutions over an algebraic closure, not over the reals.
The original result
- Claim. There is an absolute integer j such that the truth of sentences ∃x ∈ ℝr ∀y ∈ ℝs Φ(x, y) lies in the j-th level CjP of the counting hierarchy (Theorem 1.1). Here Φ is a Boolean combination of polynomial equalities and inequalities whose polynomials are given by arithmetic circuits, and j does not depend on the numbers of variables, the degrees or the coefficient sizes. For the existential fragment the manuscript gives the explicit bound ETR ∈ C26P, hence ∃ℝ ⊆ C26P (Theorem A.1).
- Source. The manuscript Existential–universal real sentences in the counting hierarchy, dated 4 October 2026 (repository commit
1581d4c). - Formalization. The repository has no Lean scope note for this family (checked 16 October 2026).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 16 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Alex Meiburg, arXiv:2610.10514 (v1) | Parallel work | The existential theory of the reals lies in the counting hierarchy, with ∃ℝ ⊆ BPPC3P ⊆ C4P, the fourth level. For each fixed w, sentences with w alternating real quantifier blocks lie in C9w+17P. Further applications cover exact semidefinite feasibility, PosSLP, the square-root sum problem, geometric real counting, Euler characteristics and complex feasibility. The abstract states that the proofs were discovered by ChatGPT in conversations ending on 29 September 2026, that a group of researchers is working to digest them, and that on 6 October OpenAI released "a very similar result, with a slightly weaker bound". | arXiv preprint, version 1 (114 pages). The listed author states that he takes responsibility that the proofs appear correct but did not play a nontrivial role in developing them. |
Notes
- Dates are those shown by arXiv and by the manuscript. The list covers sources found up to the date above; it makes no priority or completeness claim.