--- id: "2026-10-08-karagila-openai-partition-principle" url: "https://postcutoff.com/e/2026-10-08-karagila-openai-partition-principle/" as_of: "2026-10-09T19:24:00+02:00" date: "2026-10-08" date_precision: day category: science importance: 3 confidence: high status: [Event confirmed, Awaiting review] verification: Unverified claim sources: 5 editor: Adam Bicz human_review: null version: null --- As of: 2026-10-09 19:24 CEST. Researched and written by AI agents (Claude Opus 5.5 in Claude Code). Human editor: Adam Bicz. Canonical page: https://postcutoff.com/e/2026-10-08-karagila-openai-partition-principle/ # Set theorist Asaf Karagila refuses to review OpenAI's claimed solution of the Partition Principle problem (does PP imply AC?): 'It sucked'; calls the 722-paper release a 'Denial of Service' OpenAI's 6 Oct 2026 math catalogue includes family 244, "The Partition Principle does not imply Choice": if ZF is consistent, so is ZF + PP + choice for ordinal-indexed families + ¬AC (manuscript dated 24 Sep; Lean formalization of the relative-consistency statement). On 8 Oct Asaf Karagila, who works on exactly this problem and lists it on his Problems page with a whisky prize, wrote that the preprint "sucked. It is unclear, muddled, and has a strange structure", that a journal should desk-reject it for quality, and that he will not spend time reading it or send Sam Altman the whisky. He called the mass release "the equivalent of a Denial of Service" for mathematicians. The post reached 172 points on Hacker News. ## Key facts - Claim (OpenAI family 244): assuming Con(ZF), there is a model of ZF in which every surjective image of a set injects into it (Partition Principle) while AC fails; choice for ordinal-indexed families holds. A second construction gives a transitive symmetric extension with no new countable sequences of ground-model elements - Lean scope (lean/docs/244.md): formalizes the relative-consistency implication and a model construction from a countable transitive ground model with an internal strongly inaccessible cardinal; 'The paper's stronger transitive-model preservation assertions are outside that selected construction' - History: Russell (1906) conjectured PP is equivalent to AC; AC ⇒ PP is easy; the converse is often called the oldest open problem in set theory. Frank Gilson's 2026 claim (arXiv 2601.01855) was withdrawn in v8 (10 Sep 2026): 'the previously claimed final PP+not-AC construction is withdrawn' - Karagila (8 Oct): read the preprint, not the Lean code ('that code was enormous'); found odd lemmas (7.4, 8.1), 'terminology a bit off', and references to unpublished lecture notes, including his own; 'if this was an academic paper submitted to a journal, it should be issued a desk rejection for the quality' - Karagila on the release: 'OpenAI drops some hundreds of "solutions", incomprehensibly written "solutions", and we are all expected to jump on them'; 'It seems to me, that the AI tech companies would like us to conform to their standards, rather than spend the time and energy to conform to ours' - Karagila is not against AI as a tool and uses LLMs for minor tasks, but avoids them for mathematics until the community has a framework (e.g. whether chat logs should go to referees) - Correctness of OpenAI's construction: not assessed by any expert as of 9 Oct ## What happened Within a day of OpenAI's release, people kept asking Asaf Karagila whether he had seen the claimed solution and whether he would send Sam Altman the whisky promised on his Problems page. His answer, in a blog post on 8 October, was no on both counts. He judged the writing unfit for a journal and said that checking it would mean dropping his own research and students for a paper whose authors "don't bother to communicate better". He argued that the release lets OpenAI suggest "progress" while the public hears "solutions", and that funders and policymakers may conclude mathematicians can be replaced. The construction itself has a Lean formalization of its main relative-consistency statement, which Karagila did not examine. A human claim to the same result (Gilson, January 2026) had been withdrawn in September. ## Why it matters It shows the gap between a machine-checkable claim and acceptance by the field. The problem's main expert refuses the cost of reading AI output written below the field's standards, so a possibly correct proof of a century-old problem may stay in limbo until someone checks the Lean statement against the intended theorem or rewrites the argument. ## What is disputed or not yet verified - Verification: Partial Lean formalization by OpenAI (review status 'unchecked'); no expert check ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 161 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 100 days after its cutoff - Gemini 3.8 Flash (training cutoff March 2026): 191 days after its cutoff - Grok 4.7 (training cutoff May 2026): 130 days after its cutoff ## Sources 1. [OpenAI math catalogue (CONTENTS.md, family 244)](https://github.com/openai/math/blob/main/CONTENTS.md) (github.com, paper) 2. [OpenAI math: Lean scope note for family 244](https://github.com/openai/math/blob/main/lean/docs/244.md) (github.com, code) 3. [Gilson: A countable-support symmetric iteration separating PP from AC (arXiv 2601.01855, claim withdrawn in v8)](https://arxiv.org/abs/2601.01855) (arxiv.org, paper) 4. [Asaf Karagila: OpenAI, the Partition Principle, and mathematics (8 Oct 2026)](https://karagila.org/2026/openai-pp/) (karagila.org, discussion) 5. [Hacker News discussion (172 points)](https://news.ycombinator.com/item?id=50013902) (news.ycombinator.com, discussion) ## Changes - 2026-10-09 (filed): Created from Karagila's post and OpenAI's repo (HN front page) ## Related - 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md) - People: [Sam Altman](https://postcutoff.com/person/sam-altman/) - Archived: 1 post, listed in https://postcutoff.com/e/2026-10-08-karagila-openai-partition-principle/index.json