we-solve (beta)

Math-2722 · mathematics · Logic

Capturing polynomial time with choiceless computation and counting

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Is every isomorphism-invariant Boolean query that is decidable in deterministic polynomial time on all finite structures definable in choiceless polynomial time with counting, allowing hereditarily finite sets of arbitrary finite rank and polynomial bounds on computation stages and intermediate objects?

Short English statement

Is every isomorphism-invariant Boolean query that is decidable in deterministic polynomial time on all finite structures definable in choiceless polynomial time with counting, allowing hereditarily finite sets of arbitrary finite rank and polynomial bounds on computation stages and intermediate objects?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2722-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2722

The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting result is manuscript 1 (family 243; 2026-09-23).

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

Go to contribution →