Lichter and Schweitzer's question: does witnessed symmetric choice strictly increase the expressive power of CPT with counting?
Choiceless polynomial time with counting (CPT) computes invariantly with hereditarily finite sets over the input atoms and cannot choose an element of a set merely because it is nonempty. Lichter and Schweitzer introduced the extension CPT+WSC by witnessed symmetric choice: a program may pick an element of an orbit provided it constructs automorphisms certifying that the choice is symmetric, so the answer stays isomorphism invariant. In Section 7 of their paper they asked whether this extension is strictly more expressive than CPT itself. Is there a Boolean query on finite structures definable in CPT+WSC but not in CPT with counting?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Finite model theory; descriptive complexity
- Posed by
- Moritz Lichter and Pascal Schweitzer
- Year posed
- 2022
- Years open
- 4y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 18 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: over a vocabulary of eight binary relations there is a CPT+WSC sentence with a single WSC operator that returns a Boolean value on every finite structure and whose true-model class is not defined by any CPT sentence, even with counting and unbounded set rank; so CPT+WSC is strictly more expressive than CPT in Lichter and Schweitzer's sense. Not shown: whether CPT+WSC captures polynomial time, or the effect of nested WSC operators, both of which the paper leaves open.
What the AI did
The release README says the vast majority of results were obtained with one fixed procedure using an unreleased internal OpenAI model, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier results produced by the models. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region, whose write-up was human edited). The manuscripts are authored 'OpenAI' and name no human author. This entry's manuscript (September 24, 2026) is the companion of the CPT noncapture paper in the same family and has a Lean formalization of its main theorem.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against Lichter-Schweitzer's Section 7 question. Lean: lean/ComparatorChallenges/WitnessedChoice.json exists with solution module OAI.Computability.WitnessedChoice.Main present at the pinned commit; it is not listed in lean/formalization.yaml. Its statement WitnessedChoice.main asserts a sentence with exactly one WSC occurrence, Boolean on all inputs, whose true-model class differs from that of every CPT sentence. This is the headline claim, relative to the challenge file's own encoding of both formalisms, which was not audited here. Not rebuilt here.
Sources
- Lean proofLean statement: WitnessedChoice.lean (comparator challenge)Lean solution module OAI/Computability/WitnessedChoice/Main.lean
- CodeOpenAI math release: Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting
- Problem recordLichter and Schweitzer, Choiceless Polynomial Time with Witnessed Symmetric Choice (arXiv 2205.14003)