Does the Partition Principle imply the Axiom of Choice?
The Partition Principle (PP) says that whenever there is a surjection from a set onto a set , there is an injection from into ; equivalently every partition of a set injects into the set. Over ZF the Axiom of Choice implies PP, and PP implies choice for well-orderable families. The converse is the old question: does PP imply AC over ZF? Equivalently, is ZF + PP + AC consistent relative to ZF?
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Set theory; choice principles and symmetric models
- Posed by
- Classical open problem of choiceless set theory; the principle is traced to Beppo Levi (1902)
- Year posed
- —
- Years open
- —
- 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
- 45 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: Con(ZF) implies Con(ZF + PP + ACwo + AC). Theorem 1.2: over every countable transitive model of ZFC there are a set forcing and a transitive symmetric submodel with , the same ordinals, ZF + PP + ACwo + AC, and no new countable sequences of elements of . The construction makes every non-wellorderable image of a fixed set bijective with it and uses Ryan-Smith's local-to-global reduction. Remarks draw consequences for the dual Cantor-Schroeder-Bernstein principle and the Weak Partition Principle. It does not settle whether the Weak Partition Principle implies AC or PP, nor other cardinal-comparison principles beyond those remarks.
What the AI did
The release README says every result in it was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. 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). The manuscript is authored 'OpenAI' and names no human author. The manuscript (September 24, 2026) has no companion in the release.
Verification
No independent mathematician has checked this yet. Checked here: Theorems 1.1 and 1.2 of the manuscript were read against the question; Theorem 1.1 (if ZF is consistent, so is ZF + PP + ACwo + not AC) answers it as posed. lean/formalization.yaml lists PartitionPrinciple (declaration ...TransitiveGround.exists_model_partitionPrinciple_without_choice, file OAI/SetTheory/PartitionPrinciple/Models/Separation.lean). Its comparator statement was read: it assumes a countable transitive ground with an internal strongly inaccessible cardinal and yields a transitive ZF model of PP with Choice failing, which is narrower than the paper's Theorem 1.2 (no inaccessible, and also ACwo and no new countable sequences). A second challenge, ComparatorChallenges/PartitionConsistency.json, is not in the formalization catalogue; its solution module OAI/SetTheory/PartitionConsistency/Main.lean exists at the pinned commit, and its statement was read here: syntactic Con(ZF) implies Con(ZF + PP + ACwo + not AC) for an explicit first-order natural deduction over the pure membership language. That is the headline. Neither was rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.
Sources
- Lean proofLean proof (transitive-ground construction)Comparator statement: PartitionPrinciple.leanLean proof (relative consistency, not in formalization catalogue)Comparator statement: PartitionConsistency.lean
- CodeOpenAI math release: The Partition Principle does not imply Choice
- Problem recordBlass and Kulshreshtha, Cardinal well-foundedness and Choice (lists PP implies AC as open)