∑math20

Combinatorics · Result 190

Polynomial removal fails for ordered binary matrices

1 paperLean

Disproves polynomial ordered binary matrix removal with one fixed \(66\times66\) zero–one pattern. Matrices can require many binary-entry changes to become pattern-free while their copy density is smaller than every proposed polynomial bound in that distance. Copies preserve row and column orders and match both zeros and ones.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Polynomial removal fails for ordered binary matrices

Polynomial removal fails for ordered binary matrices

OpenAI · September 25, 2026

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.

Read PDF Download Source

Cite
@misc{OAI:Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026,
  author = {{OpenAI}},
  title = {{Polynomial removal fails for ordered binary matrices}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026/paper.pdf}{OAI:Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result disproves a polynomial removal bound for one explicit \(66\times66\) binary pattern. For every \(c,C>0\), there is an \(n\times n\) binary matrix at normalized edit distance at least \(\varepsilon>0\) from being pattern-free but with fewer than \(c\varepsilon^C n^{132}\) induced ordered copies. Row and column indices are independently increasing, and every zero and one entry must match. The construction gives an explicit sequence of such matrices, allowing edits in both directions.

Comparator links

ResultComparator statement
Failure of polynomial removal for ordered binary matricesMatrixRemoval.lean

Scope note on GitHub →