OpenAI, the Partition Principle, and Mathematics
OpenAI announced that the Partition Principle does not imply the Axiom of Choice. Whether it does is an open question over ZF, listed on Karagila's own open-problems page. Karagila, who has worked on Choice for more than 15 years, read the preprint but skipped the Lean code, saying he knows little Lean and the code was enormous. He found the paper unclear and strangely structured, with terminology that seemed off. The Lean statement file alone is 277 lines, with home-built syntax for formulas, satisfaction and ZF axiom schemas. The paper was part of a bulk release. OpenAI posted 372 families of AI-generated results on October 6 and withdrew three manuscripts the next day over a sign error. 300 of 719 top-line results, about 42%, had machine-checked Lean proofs. The same week, Terence Tao and Scott Aaronson published commentary and the Erdős problems site froze proof claims. For AI builders, the lesson is that a passing formal check does not make output readable or credible to the experts who have to judge it. As generation scales, unpaid reviewers carry the checking work, and trust depends on clear artifacts more than on volume.
