Is there a logic for polynomial time?
Two preprints claim that choiceless polynomial time with counting does not capture polynomial time
Covers result 243 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.
4:32. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A computer always stores a graph in some order and algorithms use it; a logic sees only the graph. With an ordering supplied, Immerman and Vardi showed in 1982 that fixed-point logic expresses exactly the polynomial-time properties; without one, Gurevich conjectured that no logic captures polynomial time. The leading remaining candidate is choiceless polynomial time, introduced by Blass, Gurevich and Shelah: a parallel program over sets built from the input that may form “the set of all” and, in its extended version, count, but never “pick one”. Their 1997 preprint conjectured that even with counting it falls short of polynomial time. The best earlier lower bound for a yes-or-no question, by Dawar, Richerby and Rossman, needed a cap on how deeply sets nest.
Result 243 is two OpenAI preprints, dated September 23 and 24, 2026. The first claims a polynomial-time property of unordered finite structures, consistency of a linear system over 𝔽3 read off eight relations, that choiceless polynomial time with counting cannot express at any nesting depth of sets, confirming the Blass–Gurevich–Shelah conjecture (Shelah had claimed such a result in 2000, but the problem was still treated as open). The second claims that adding witnessed symmetric choice, an operator of Lichter and Schweitzer, strictly increases expressive power: one sentence with one such choice defines a property no choiceless program can, and tells the same two charged grids apart.
What it doesn’t claim
That no logic captures polynomial time (which would imply P ≠ NP); anything about the classic Cai–Fürer–Immerman graphs; explicit sizes.
Where it stands
- Posted as preprints
- OpenAI, 2 papers, 79 pages, dated September 23 and 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Yes, both theorems (docs)
Last checked October 19, 2026. The preprints have not been revised since release. In Lean, both theorems are formalized, about 18,000 and 26,000 lines with no unproved steps, each defining choiceless polynomial time from scratch in its own way (we did not build them); the repository’s notes contradict themselves about whether the second result is included. OSVerify has not reviewed them, and we found no expert reaction.
How the proof goes
- Two charged grids. On an L × L × L grid, each edge carries states and each vertex carries configurations, with a charge at every vertex: all zero in one structure, a single one in the other. The linear system is consistent for charge zero and inconsistent for a single charge.
- Short supports at any depth. A symmetry group of Heisenberg type, whose translations commute only up to a central correction, forces every object a polynomial computation builds to be pinned down, for the key symmetries, by a short list of elements, whatever the nesting depth of its sets. Counting logic with about L7/4 variables cannot tell the grids apart, and that transfers to every set the program can build.
- Large L. So a fixed program gives the same answer on both grids once L is large enough, while the true answers differ. The witnessed-choice sentence instead picks one edge state at a time, each pick certified by exhibiting symmetries.
The numbers in the video
- Ours: the smallest grids the paper allows (L = 2) have 55,404 elements; the symmetry group has 317 ≈ 129 million elements and 20 orbits, one per block. Reading the system off the relations: consistent for charge zero (rank 55 = 55), inconsistent for each of the 8 single-charge placements (55 vs 56).
- Ours: from the paper’s inequalities, the proof needs L of at least about 1047. Running the witnessed-choice procedure on the L = 2 grids accepted 6 of 6 charge-zero runs and rejected 6 of 6 single-charge runs.
Read the source
The 2 papers in this result
OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.
Transcript
Read the full script
0:00The question
A computer always stores a graph in some order, and algorithms use it: start at the first vertex. A logic sees only the graph itself. With an ordering supplied, Immerman and Vardi showed in 1982 that fixed-point logic expresses exactly the polynomial-time properties. Without one, Gurevich conjectured that no logic captures polynomial time. The leading remaining candidate is choiceless polynomial time, introduced by Blass, Gurevich and Shelah: a parallel program over sets built from the input, allowed to form the set of all objects of a kind, and in its extended version to count, but never to pick one. Their 1997 preprint conjectured that even with counting it falls short of polynomial time. The best earlier lower bound for a yes-or-no question, by Dawar, Richerby and Rossman, needed a cap on how deeply sets nest. Choice is the issue because of symmetry. On the smallest grid the paper allows, we count 55,404 elements, and a symmetry group of 3^17, about 129 million elements, mixes the elements attached to each edge, and to each vertex, completely: inside such a block, every element looks like every other, and a choiceless program cannot single one out.
1:21The claim
Result 243 is two OpenAI preprints, dated September 23 and 24, 2026. The first claims a polynomial-time property of unordered finite structures, consistency of a linear system over the field with three elements, read off eight relations, that choiceless polynomial time with counting cannot express, at any nesting depth of sets. That would confirm the Blass, Gurevich and Shelah conjecture. Shelah had claimed such a result in 2000, but the problem was still treated as open. The second claims that adding witnessed symmetric choice, an operator of Lichter and Schweitzer, strictly increases expressive power: one sentence with one such choice defines a property no choiceless program can, and it tells the same two charged grids apart. Not claimed: that no logic captures polynomial time, which would imply P ≠ NP; anything about the classic Cai, Fürer and Immerman graphs; or explicit sizes.
2:22How the proof goes
The witnesses are two grids of size L by L by L. Each edge carries states, each vertex carries configurations, and a charge sits at every vertex: all zero in one structure, a single one in the other. Reading the linear system off the relations, our computer found it consistent for charge zero and inconsistent for each of the 8 single-charge placements on the smallest grid. The key is the symmetry group, of Heisenberg type: translations that commute only up to a central correction. Its commutators force every object a polynomial computation builds to be pinned down, for the key symmetries, by a short list of elements, whatever the nesting depth of its sets. Then, with counting logic using about L^(7/4) variables, the two grids look the same, and that transfers to every set the program can build. So a fixed program gives the same answer on both grids once L is large enough, while the true answers differ. How large does the proof need? By our arithmetic from the paper’s inequalities, at least about 10^47. The witnessed-choice sentence, in contrast, picks one edge state at a time, each pick certified by exhibiting symmetries. We ran its procedure on the smallest pair of grids: it accepted all six charge-zero runs and rejected all six with a single charge.
3:46Where it stands
The preprints are unrefereed and unchanged since release. In Lean, both theorems are formalized, about 18,000 and 26,000 lines with no unproved steps, each defining choiceless polynomial time from scratch in its own way. We did not build them, and the repository’s notes contradict themselves about whether the second result is included. OSVerify has not reviewed them, and we found no expert reaction. If they hold, choiceless polynomial time with counting, long a leading candidate for a logic of polynomial time, does not capture it; witnessed choice is still in the running, and the search for such a logic, or a proof that none exists, goes on.
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.