OpenAI, the Partition Principle, and mathematics
B · Useful, limited Blog post by set theorist Asaf Karagila, a specialist on the Axiom of Choice, giving an expert first-hand reading of OpenAI's preprint; credible and specific, but opinion without systematic data.
Summary based on the full text·Original: about 7 minutes to read
In short
Asaf Karagila, a set theorist who has worked on the Axiom of Choice for over 15 years and publicly offered a bottle of whisky for a solution, reviews OpenAI's announcement (October 2026) that the Partition Principle does not imply the Axiom of Choice. He read the preprint, not the Lean formal proof. His verdict: the paper is unclear, oddly structured and badly referenced, and would deserve a desk rejection. His larger complaint is that AI labs publish hard-to-read "solutions" and leave experts to do the checking.
Key numbers
- over a centuryage of the Partition Principle versus Axiom of Choice problem OpenAI claims progress on
- at least threeunpublished, unrefereed, non-arXiv lecture notes cited as references in the OpenAI preprint
- over 15 yearsthe author's time working on the Axiom of Choice
As reported by the source.
English·Web page·opens karagila.org
What it reports
- Several colleagues contacted him within a day of the announcement, asking whether he would pay out the whisky; he will not.
- The preprint's terminology is "a bit off"; specific lemmas (7.4, 8.1) are results he would not expect in such a paper, stated strangely.
- References are weak: one of his Bristol model papers is cited for basic symmetric extensions, and at least three unpublished, unrefereed lecture notes are cited, including his own, for a proposition available in published work.
- He says he normally grasps the strategy of an Axiom of Choice paper on a skim; with this preprint that was impossible.
- He calls a release of hundreds of badly written "solutions" a denial-of-service on expert time, while press coverage converts "progress" into "solutions".
- He notes arXiv introduced rate limiting in response to AI-generated submissions, and that most papers now carry an AI-use statement.
- He proposes that experts be consulted before release, and asks whether chat logs should be available to reviewers.
How they got it
A personal reading of the preprint by a domain expert. The Lean code was not checked, by the author's own statement. No independent verification of the result is offered either way.
Limits
- Judges presentation and scholarly quality, not correctness; the formal Lean proof may still be valid.
- A single expert's view, written within a day of the announcement.
Why it matters for companies
The same pattern appears inside companies: AI output that may be correct but is costly to verify shifts work from the producer to the reviewer. Counting "problems solved" without counting expert review hours overstates the gain. Teams adopting AI for analysis or drafting should set standards for readability and sourcing, and decide who carries the checking cost, before volume rises.
Summary based on the full text. Read the original for the full argument and data.Read the original on karagila.org