Separating choiceless counting from polynomial time and witnessed choice

2 papersLean

Confirms the Blass–Gurevich–Shelah noncapture conjecture: consistency of a linear system over 𝔽₃ 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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Choiceless polynomial time with counting does not capture polynomial time

OpenAI · September 23, 2026

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 𝔽₃ in a fixed binary vocabulary is decidable in polynomial time but not in the full counting formalism.

Read PDF Download Source

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}
}

Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting

OpenAI · September 24, 2026

We prove that witnessed symmetric choice strictly increases the expressive power of choiceless polynomial time with counting. A fixed sentence with one witnessed-choice occurrence defines a Boolean query on every finite input that is not definable in the original counting formalism.

Read PDF Download Source

Cite

@misc{OAI:Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026,
  author = {{OpenAI}},
  title = {{Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026/paper.pdf}{OAI:Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result separates polynomial time from choiceless polynomial time with counting. It gives an explicit query on finite structures with eight relations that is invariant under isomorphism and decidable in polynomial time, but is not definable in the stated hereditarily finite-set language with cardinality and polynomial bounds on stages and intermediate objects. The query applies to all finite inputs without a promise. The separate witnessed-symmetric-choice result is not included.

The formalization proves that witnessed symmetric choice strictly increases the expressive power of choiceless polynomial time with counting. It constructs one fixed sentence with exactly one witnessed-choice occurrence that gives a Boolean answer on every finite input, while no sentence of the original counting formalism defines the same class of inputs.

Comparator links

Result	Comparator statement
Polynomial-time query outside choiceless polynomial time	ChoicelessPolynomialTime.lean
Strict expressive gain from one witnessed symmetric choice	WitnessedChoice.lean

Scope note on GitHub →