The Partition Principle and the Axiom of Choice
From OpenAI Aftermath
The Partition Principle and the Axiom of Choice concerns a question in set theory without choice. The Partition Principle says that whenever a set X maps onto a set Y, there is an injection from Y into X; equivalently, every partition of a set injects into that set. The Axiom of Choice implies it, and whether the converse holds has been open since the early twentieth century. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a negative answer: if ZF is consistent, then so is ZF together with the Partition Principle, Choice for well-orderable families, and the failure of the Axiom of Choice. The collection includes Lean formalizations of this relative-consistency statement and of a model construction. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Da Silva traces the Partition Principle to Beppo Levi in 1902. Banaschewski and Moore studied its relation to the dual Cantor–Schröder–Bernstein theorem and neighbouring cardinal-comparison principles, and Blass and Kulshreshtha's August 2026 version still lists the implication from the Partition Principle to Choice as open. Gilson's September 2026 corrections withdraw the model-construction claims of three earlier approaches.
- The implication from the Partition Principle to Choice for well-orderable families is classical (an argument attributed to Pincus, recorded by Ryan-Smith). Blass's small violations of choice and Ryan-Smith's local-to-global criteria reduce the Partition Principle to statements about one fixed set of parameters.
- The method is a symmetric submodel of a set-forcing extension; a specific antecedent is Holy and Schilhan's product of Cohen forcing with a forcing of hereditarily almost-disjoint towers, which builds on Pincus's work on Dependent Choice.
The original result
- Claims. Theorem 1.1 of The Partition Principle does not imply Choice states that if ZF is consistent, then so is ZF + PP + ACWO + ¬AC, where PP is the Partition Principle and ACWO is Choice for families indexed by ordinals. Theorem 1.2 gives a transitive form: for every countable transitive model V of ZFC there are a forcing, a generic filter and a transitive symmetric submodel W of the extension, with the same ordinals as V, satisfying ZF + PP + ACWO + ¬AC, and with no new countable sequences of elements of V.
- Method, as described: the forcing adds a set A of distinct generic subsets of ω1 that cannot be well-ordered in the symmetric model, while every set is a surjective image of A × η for some ordinal η. The central property is that every non-well-orderable surjective image of A is in bijection with A; the coherent bijections are produced through a left-cancellative monoid of diagrams that controls supports and quotient multiplicities. Ordinal-indexed choice then assembles reverse injections for arbitrary surjections.
- Sources. The manuscript The Partition Principle does not imply Choice at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization proves the relative-consistency implication: if ZF is consistent, then so is ZF with the Partition Principle, Choice for ordinal-indexed families and the failure of Choice. It also constructs a transitive model of the Partition Principle without Choice from an externally countable transitive ground model of the stated axioms, including Choice, that contains an internal strongly inaccessible cardinal; the paper's stronger transitive-model preservation assertions are outside that construction. The Comparator statements are
PartitionConsistency.leanandPartitionPrinciple.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 21 October 2026) |
|---|---|---|---|---|
2026-10-07 (latest commit 0d56c31, 15 October 2026) |
F. Cançado, frederico-cancado/AC-zoo-results (GitHub) | Use (consequences in the model) | A preliminary note and a 40-page report of 7 October on weak choice principles in the manuscript's model. From the model's structural hypotheses the note derives a finite coinitial basis for the injection order on cardinalities, with consequences that include the absence of infinite strictly decreasing sequences of cardinalities and of infinite set-sized antichains of cardinalities in that model. It does not prove these consequences from the Partition Principle alone, and the status of the Partition Principle and the Boolean prime ideal theorem in a finite-order extension of the model is left unresolved. | Preliminary drafts, not peer reviewed; the README states that they were prepared with substantial assistance from OpenAI Codex, that separate AI audits are not human review, and that the new deductions are not formalized. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial" and records a Comparator pass for PartitionConsistency, stated with a hand-coded first-order calculus for ZF; PartitionPrinciple was not run. Its note states that the transitive-model theorem appears only as a construction that needs an internal strongly inaccessible cardinal in the ground model and does not include ordinal-indexed choice or the property about countable sequences, and it lists the hand-written encoding of ZF among the definitions to check, since an encoding that made ZF inconsistent would make the implication vacuous. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38051470892 (PartitionConsistency, PartitionPrinciple) |
Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept both solutions, in 479 s and 3,218 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) lists neither challenge, so both were accepted by con-leche and by Lean's official kernel. |
Development journal. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
