Browse › Mathematical logic › 243 Separating choiceless counting from polynomial time and witnessed choice
Choiceless polynomial time with counting does not capture polynomial time
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
We prove that choiceless polynomial time with counting does not capture polynomial time on unordered finite structures, confirming the noncapture conjecture of Blass, Gurevich and Shelah. A linear-consistency query over 𝔽3 in a fixed binary vocabulary is decidable in polynomial time but not in the full counting formalism.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI, Lean scope notes for family 243 (release documentation, October 2026). Describes the formalized statement as an explicit isomorphism-invariant polynomial-time query on eight-relation structures, with no promise on the input, that is not definable in the formalized counting HF-set language with polynomial bounds. [family-level]
- OpenAI, ComparatorChallenges/ChoicelessPolynomialTime.lean (openai/math, commit adc7f12). This comparator file specifies the target statement combining isomorphism invariance, ordinary polynomial-time decidability and nondefinability in its full-CPT evaluation language, with the target proof left as a placeholder.
- OpenAI, OAI/ModelTheory/Choiceless/Separation.lean (openai/math, commit adc7f12). Proves
CPTSeparation.main: the query is isomorphism-invariant, it is inOrdinaryPolynomialTime, and it is notFullCPT.EvaluationDefinable.
Related prior literature mentioned by others
- Andreas Blass, Yuri Gurevich and Saharon Shelah, Choiceless polynomial time (arXiv:math/9705225v1, 15 May 1997). The AI Proved What? exposition identifies this work as the source of the choiceless model and the counting noncapture conjecture motivating the family. [family-level]
- Anuj Dawar, David Richerby and Benjamin Rossman, Choiceless Polynomial Time, Counting and the Cai–Fürer–Immerman Graphs (author preprint, 13 August 2007; Annals of Pure and Applied Logic, 2008). The AI Proved What? exposition contrasts this work's rank-restricted counting lower bounds with the family's claimed separation allowing unrestricted finite set rank. [family-level]
Possibly relevant literature (found by the agent, not checked)
- Moritz Lichter, Separating Rank Logic from Polynomial Time (arXiv:2104.12999; J. ACM 70(2), 2023; LICS 2021). Shows that rank logic does not contain CPT, using CFI graphs over Z_{2^i}, the converse non-containment to the paper's Corollary 1.3 that FPR_3 is not contained in CPT.
Digests and expositions
- AI Proved What?, Is there a logic for polynomial time? (episode 243, October 2026). This AI-assisted video and transcript outline both separating queries, the charged-grid construction and the rank-independent support argument, and report small-grid computations performed for the exposition. [AI-generated per source] [family-level]
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 243
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026,
author = {{OpenAI}},
title = {{Choiceless polynomial time with counting does not capture polynomial time}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026/paper.pdf}{OAI:Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/243.md. The Lean statements have not been checked by people against the paper's claims.
Family 243: Separating choiceless counting from polynomial time and witnessed choice
Confirms the Blass–Gurevich–Shelah noncapture conjecture: consistency of a linear system over 𝔽3 defines a polynomial-time query on unordered finite structures that choiceless polynomial time with counting cannot express. A separate result shows that adding witnessed symmetric choice strictly increases expressive power. Both separations hold for the full counting formalism, allowing hereditarily finite sets of arbitrary finite rank.
Other papers in this family: