OpenAI claim summary for Math-2722

Capturing polynomial time with choiceless computation and counting

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 243; 2026-09-23), the asserted result is that a fixed linear-consistency query over $\mathbb F_3$ is polynomial-time decidable but not definable in choiceless polynomial time with counting on all unordered finite structures.

Mathematical statement of the claimed result

Manuscript 1.

The finite vocabulary has eight binary relations $\mathsf{Ed},\mathsf{Cf},\mathsf{EB},\mathsf{VB},\mathsf I,\mathsf Z_0,\mathsf Z_1,\mathsf Z_2$. In a structure $A$, set $Y=\{y:\mathsf{Ed}(y,y)\}$, $X=\{a:\mathsf{Cf}(a,a)\}$ and $X_t=\{a\in X:\mathsf{VB}(t,a)\}$. Over $\mathbb F_3$ put \[ C(y,a)=\sum_{\substack{x\in Y\\\mathsf I(a,x)}}\ \sum_{\substack{\delta\in\mathbb F_3\\\mathsf Z_{\delta}(y,x)}}\delta. \] Define $Q(A)$ as consistency of unknowns $(\lambda_a)_{a\in X},(\mu_y)_{y\in Y}$ satisfying \[ \sum_{a\in X_t}\lambda_a=1\ (t\in X),\qquad \mu_y=\sum_{a\in X_t}\lambda_a C(y,a) \] for those pairs $(t,y)$ having some $a\in X_t,x\in Y$ with $\mathsf I(a,x)$ and $\mathsf{EB}(y,x)$. The claim is that $Q$ is an isomorphism-invariant polynomial-time query on all finite structures while no sentence of CPT with counting defines $Q$, even when set ranks are unbounded.

Outline of the argument

For manuscript 1 (family 243; 2026-09-23), charged three-dimensional grids have opposite consistency answers. Central-extension automorphisms force small constructed objects to have sparse supports, and counting-equivalent grids preserve every fixed-program state and output despite their different total charges.

Formal verification

For manuscript 1 (family 243; 2026-09-23), OpenAI lists Lean statements for this assertion: a fixed linear-consistency query over $\mathbb F_3$ is polynomial-time decidable but not definable in choiceless polynomial time with counting on all unordered finite structures.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are ChoicelessPolynomialTime.lean, WitnessedChoice.lean.

Their named declarations include OAI.CPTSeparation.main, OAI.WitnessedChoice.main.

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, Choiceless polynomial time with counting does not capture polynomial time, 2026-09-23; citation key OAI:Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 243: Lean scope.
• Comparator ChoicelessPolynomialTime.json.
• Comparator ChoicelessPolynomialTime.lean.
• Comparator WitnessedChoice.json.
• Comparator WitnessedChoice.lean.
• OpenAI catalogue entry.