Oct 6, 2026
Lean formalization in OpenAI math repository (Result 190)
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 'Polynomial removal fails for ordered binary matrices'. We construct a fixed 66\times66 binary matrix for which ordered matrix removal has no polynomial bound. This disproves the polynomial ordered binary matrix-removal conjecture. Ordered copies preserve the separate row and column orders and match both zeros and ones; removal permits changing entries in either direction.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 190). The Lean development was not rebuilt locally.