No more pieces than points, yet no choice?
A preprint claims that the Partition Principle does not imply the Axiom of Choice
Covers result 244 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:16. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Cut a set into pieces. The Partition Principle says there are never more pieces than points: some one-to-one map sends each piece to a point. The Axiom of Choice gives such a map at once, by picking a point from every piece, but the Partition Principle asks for less: the point need not lie in its piece. For six points in pieces of sizes 1, 2 and 3 there are 120 one-to-one maps from pieces to points, and only 6 pick each piece’s point from inside it. For finite sets both always exist; the question is about infinite ones. Beppo Levi stated the principle in 1902, and Russell claimed, without proof, that it implies choice. Asaf Karagila has called the question the oldest open problem in set theory. Between November 2025 and January 2026 Frank Gilson posted three preprints claiming such a model; by September 2026 he had withdrawn the claims in all three.
Result 244 is one OpenAI preprint, 44 pages, dated September 24, 2026. It claims that if ZF is consistent, so is ZF plus the Partition Principle plus the failure of choice. Choice for ordinal-indexed families still holds there, but that already follows from the Partition Principle, as Pincus showed. A second deduction, from any countable transitive model with choice, gives a transitive symmetric extension with the same properties, the same ordinals, and no new countable sequences of old sets.
What it doesn’t claim
That choice is false or unneeded: choice still implies the Partition Principle. No atoms and no large cardinals are used.
Where it stands
- Posted as a preprint
- OpenAI, 44 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Yes, the headline consistency statement (docs)
Last checked October 19, 2026. The preprint has not been revised since release. In Lean, the headline consistency statement is formalized with set-theoretic syntax built from scratch, about 33,000 lines with no unproved steps; the Lean proof builds the model outright in Lean’s stronger logic rather than following the paper’s argument from ZF alone. A larger transitive-model version assumes an inaccessible cardinal, which the paper avoids. We did not build them. OSVerify has not reviewed it. Asaf Karagila sharply criticized the paper’s exposition, terminology and references, declined to read further, and trusts the Lean statement but not the code; he gave no verdict on correctness.
How the proof goes
- A reduction. Following Ryan-Smith’s method: if every set is an image of one special set A times an ordinal, choice holds for ordinal-indexed families, and every image of A that cannot be well-ordered is the same size as A, then the Partition Principle holds.
- The model. Add many new subsets of the first uncountable cardinal, which serve as labels and form A, and keep only the sets that survive enough permutations of them. Supports are too small to list all the labels in order, so A cannot be well-ordered and choice fails. A second forcing lays copies of a custom-built monoid, called diagrams, over the labels; the monoid controls how groups of labels can overlap and combine.
- The heart. Theorem 6.3: every image of A that cannot be well-ordered is put in bijection with A, coherently across all symmetries. Choices inside the new model must respect every symmetry, so countably many bits of the new sets serve as fingerprints that pick out one of countably many candidates, and the pick moves along with every symmetry.
The numbers in the video
- Ours: for pieces 1, (2, 3), (4, 5, 6) there are 120 one-to-one maps from pieces to points, and 6 pick from inside.
- Ours: the reduction’s bookkeeping checked on 2,000 random finite cases.
Read the source
- The Partition Principle does not imply Choice (PDF), 44 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 244.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Cut a set into pieces. The Partition Principle says there are never more pieces than points: some one-to-one map sends each piece to a point. The axiom of choice gives such a map at once, by picking a point from every piece. But the Partition Principle asks for less: the point need not lie in its piece. Here are 6 points cut into pieces of sizes 1, 2 and 3. There are 120 one-to-one ways to send the three pieces to points, and only 6 of them pick each piece’s point from inside it. For finite sets both always exist; the question is about infinite ones. Beppo Levi stated the principle in 1902, and Russell claimed, without proof, that it implies choice. In set theory without choice, does the Partition Principle prove the axiom of choice? Asaf Karagila has called it the oldest open problem in set theory. Between November 2025 and January 2026, Frank Gilson posted three preprints claiming such a model; by September 2026 he had withdrawn the claims in all three.
1:04The claim
Result 244 is one OpenAI preprint, 44 pages, dated September 24, 2026. It claims that if ZF (Zermelo–Fraenkel set theory) is consistent, so is ZF plus the Partition Principle plus the failure of choice. So the Partition Principle does not prove choice. Choice for families indexed by ordinals still holds there, but that already follows from the Partition Principle, as Pincus showed. A second deduction, from any countable transitive model with choice, gives a transitive symmetric extension with the same properties, the same ordinals, and no new countable sequences of old sets. Not claimed: that choice is false, or unneeded; choice still implies the Partition Principle. No atoms and no large cardinals are used.
1:56How the proof goes
First, a reduction, following Ryan-Smith’s method. If every set is an image of one special set A times an ordinal, if choice holds for ordinal-indexed families, and if every image of A that cannot be well-ordered is the same size as A, then the Partition Principle holds. We checked the bookkeeping of this step on 2,000 random finite cases. Then build a model where A behaves that way: add many new subsets of the first uncountable cardinal, which serve as labels and form the set A, and keep only the sets that survive enough permutations of them. Supports are too small to list all the labels in order, so A cannot be well-ordered, and choice fails. A second forcing lays copies of a custom-built monoid, called diagrams, over the labels, and the monoid controls how these groups of labels can overlap and combine. The heart is Theorem 6.3: every image of A that cannot be well-ordered is put in bijection with A, coherently across all the symmetries. Choices made inside the new model must respect every symmetry, so the paper lets the generic data choose: countably many bits of the new sets serve as fingerprints that pick out one of countably many candidates, and the pick moves along with every symmetry.
3:14Where it stands
The preprint is unrefereed and unchanged since release. In Lean, the headline statement, consistency relative to ZF, is formalized with set-theoretic syntax built from scratch, about 33,000 lines with no unproved steps, though the Lean proof builds the model outright in Lean’s stronger logic rather than following the paper’s argument from ZF alone; a larger transitive-model version assumes an inaccessible cardinal, which the paper avoids. We did not build them. OSVerify has not reviewed it. Karagila sharply criticized the paper’s exposition, terminology and references, declined to read further, and trusts the Lean statement but not the code; he gave no verdict on correctness. If it holds, the Partition Principle is strictly weaker than choice: there is a world where no partition has more pieces than points, yet some partition has no way to pick a point from every piece.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.