Oct 6, 2026
Lean formalization in OpenAI math repository (Result 185)
Model / AI: OpenAI (unreleased)
machine-checked (counterexample)self-reported (counterexample)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Counterexample to the Infinite Matroid Packing/Covering Conjecture'. We construct in ZFC two self-dual partitional matroids on a countably infinite common ground set that admit neither a packing/covering partition nor an intersection witness. This disproves the unrestricted infinite matroid packing/covering and intersection conjectures and answers Joó's question for two partitional matroids negatively. The examples are neither finitary nor cofinitary.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 185). The Lean development was not rebuilt locally.