Oct 6, 2026
Lean formalization in OpenAI math repository (Result 244)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Partition Principle does not imply Choice'. We prove that the Partition Principle does not imply the Axiom of Choice: if ZF is consistent, then so is ZF with the Partition Principle, Choice for ordinal-indexed families, and the negation of the Axiom of Choice. Separately, over every countable transitive model of ZFC, we construct a transitive symmetric model of this theory with the same ordinals and no new countable sequences of ground elements.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 244). The Lean development was not rebuilt locally.