oai-math-revised beta

Browse › Mathematical logic › 243 Separating choiceless counting from polynomial time and witnessed choice

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

OpenAI · September 24, 2026

Lean

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

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). The first scope paragraph says the witnessed-symmetric-choice result is not included, while a second paragraph and a comparator link (WitnessedChoice.lean) in the same notes describe a formalization of this result. [family-level]
  • OpenAI, ComparatorChallenges/WitnessedChoice.lean (openai/math, commit adc7f12). States WitnessedChoice.main : BGS.MainStatement, proof left as sorry in this file: there is a sentence with exactly one wsc operator that is Boolean on all finite inputs, and no wsc-free sentence has the same models.
  • OpenAI, OAI/Computability/WitnessedChoice/Main.lean (openai/math, commit adc7f12). Proves main : BGS.MainStatement by instantiating the separating sentence and evaluating it on a zero-charge grid input (true) and a unit-charge input (false).

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

Independent sites; their content is not reviewed here.

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

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: