Choiceless polynomial time with counting

Choiceless polynomial time with counting is a model of computation on unordered finite structures, introduced by Blass, Gurevich and Shelah, in which a program builds hereditarily finite sets over the input elements, may count, and never chooses an element arbitrarily. Its authors conjectured that it does not express every polynomial-time property of unordered structures, a question tied to Gurevich's problem whether any logic captures polynomial time. Two manuscripts in OpenAI's public mathematics collection, dated 23 and 24 September 2026, claim that conjecture and a further separation by one witnessed choice. The collection's Lean formalization states both main theorems.

Background

As recounted in the first manuscript's introduction:
- Logics for polynomial time. Immerman and Vardi showed that least fixed-point logic expresses exactly the polynomial-time queries on finite structures with a linear order. For unordered structures, Chandra and Harel asked whether the polynomial-time queries can be enumerated effectively, and Gurevich conjectured that no logic captures polynomial time.
- Choiceless computation. Blass, Gurevich and Shelah introduced choiceless polynomial time to compute over hereditarily finite sets without choosing an ordering, and their 1997 preprint conjectured that its extension by counting is still a proper fragment of polynomial time. Shelah's early work claimed noncapture for counting extensions; later accounts, through work of Dawar, Grädel, Kullmann and Pago in 2025, continued to state the problem as open. The manuscript gives a separate proof and does not use Shelah's claim.
- Earlier lower bounds. The construction of Cai, Fürer and Immerman gave a polynomial-time graph query outside fixed-point logic with counting. Dawar, Richerby and Rossman showed that its preordered version is definable without counting, while counting does not suffice when the rank of sets is restricted to o(log n/log log n); their lower bound for each fixed rank does not give a separation for the full formalism. Positive choiceless canonization results of Abu Zaid, Grädel, Grohe and Pakusa and of Lichter and Schweitzer cover further structured classes.

The original results

Noncapture, 23 September 2026. The main theorem of Choiceless polynomial time with counting does not capture polynomial time states that an explicit query on all finite structures in a fixed vocabulary of eight binary relations, the consistency over the field with three elements of a linear system read off the relations, is invariant under isomorphism and decidable in deterministic polynomial time, but is not definable in full choiceless polynomial time with counting, with no bound on the rank of sets. The manuscript states that this confirms the noncapture conjecture of Blass, Gurevich and Shelah, and derives that the solvability and rank extensions of fixed-point logic with counting over the field with three elements are not contained in choiceless polynomial time.
Witnessed symmetric choice, 24 September 2026. The main theorem of Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting states that there is a sentence of choiceless polynomial time with counting and one occurrence of the witnessed-symmetric-choice operator of Lichter and Schweitzer that has a Boolean value on every finite structure in a vocabulary of eight binary relations, while no sentence without that operator, of any rank, has the same class of true models.
Scope, as stated: the query is total on finite inputs, with no promise on the input. Excluding this candidate leaves Gurevich's broader question open.
Method, as described: for each side length L the manuscripts build two structures from a three-dimensional grid, with states on edges and configurations at vertices whose charges are all zero in one structure and a single one in the other, so that the linear system is consistent for the first and inconsistent for the second. An automorphism group containing a central subgroup of divergence-free flows, with commutators that concentrate the relevant linear functionals on few edges, gives every object of a polynomially bounded computation a short support whatever its rank. The two structures agree on counting sentences with about L^7/4 variables, and this equivalence is transferred to all supported hereditarily finite objects, so that a fixed program gives the same answer on both structures for large L.
Sources. Commit adc7f12 of the openai/math repository: Choiceless polynomial time with counting does not capture polynomial time and Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting.
Formalization. The scope note, present since the repository's first commit of 6 October 2026, links both manuscripts. It states that the Lean development proves the separation of polynomial time from choiceless polynomial time with counting for the explicit query on all finite inputs, and that it proves the witnessed-choice separation with one fixed sentence; its first paragraph also states that the witnessed-choice result is not included, which contradicts its second paragraph and its table. Comparator statements: ChoicelessPolynomialTime.lean and WitnessedChoice.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 1 November 2026)
2026-10-08	MathVet, a GitHub review of openai/math, tables at repository commit `c76f1e4` of 14 October 2026	Review, fidelity of the formal statement	Rates this family "full": both separations of the summary are stated, the noncapture theorem with Mathlib's polynomial-time Turing machines for the query and a hand-written formalism of choiceless polynomial time with counting over hereditarily finite sets of arbitrary rank, and the witnessed-choice theorem in a second, separately written term and formula logic. Among the definitions to check it lists these two encodings, and states that the nonexpressibility statements are only as good as the encodings. It records sandboxed Comparator passes on 8 October 2026, with 18,461 and 26,381 lines in the dependency cones.	Review repository. Read on 1 November 2026.
2026-10-10	cert-machine, openai/math lane K, run 38051470892	Verification, two kernels	Records the challenges `ChoicelessPolynomialTime` and `WitnessedChoice` as certified: Lean's default kernel and the nanoda kernel both accept the solutions, in 387 s and 719 s. C. Toledo's report lists the lane's results.	Repository. The run concerns the formalized statements only.
2026-10-10 to 2026-10-14	con-leche development journal, task #348	Verification, second kernel	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions lists neither of this family's challenges, so both were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-17	AI Proved What?, episode 243 Is there a logic for polynomial time?, remade version of 22 October 2026	Reading, exposition	Video explainer of the two preprints, of 34 and 45 pages. It recalls Immerman and Vardi, Gurevich's conjecture, the model of Blass, Gurevich and Shelah and the rank-bounded lower bound of Dawar, Richerby and Rossman, notes Shelah's claim of 2000, and states that the result does not show that no logic captures polynomial time and says nothing about the classic Cai–Fürer–Immerman graphs. It reports its own checks on the smallest grids the papers allow: 55,404 elements, the linear system consistent for zero charge and inconsistent for each of eight single-charge placements, and the witnessed-choice procedure accepting and rejecting as predicted, and it estimates from the papers' inequalities that the proof needs a side length of about 10⁴⁷.	Episode status, last checked 30 October 2026: posted as preprints, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, both theorems, with the scope note contradicting itself about the second; no expert reaction found. The site states that it is made with Anthropic's Claude. Read on 1 November 2026.
2026-10-18	AI Proof Watch, record OpenAI reports a polynomial-time query outside choiceless counting	Catalogue record, assessment	Rates the importance as major, as a resolution of the noncapture conjecture for the full counting formalism, and the AI involvement as AI-led. It lists as limitations that the query is total on finite inputs in a fixed vocabulary and that the witnessed-choice extension is a separate result, and it rates the technical verification as formal, on OpenAI's reported Lean proof, and the human understanding as few, the default when no named explanation is documented.	Curated public tracker; record published 18 October 2026, assessment reviewed 31 October 2026. Read on 1 November 2026.

Notes

The background summarizes the first manuscript's own account of earlier work.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.