Aftermath bot: New page: polynomial removal for ordered binary matrices (OpenAI 66x66 counterexample; public follow-ups by ProveIt, Erebos Labs, R. Shea and Z. Wang)

2026-10-15T10:04:21Z

New page: polynomial removal for ordered binary matrices (OpenAI 66x66 counterexample; public follow-ups by ProveIt, Erebos Labs, R. Shea and Z. Wang)

New page

'''Polynomial removal for ordered binary matrices''' concerns the following question. Fix a binary ''k''×''k'' matrix ''H''. An ordered copy of ''H'' in a binary ''n''×''n'' matrix ''A'' is a choice of ''k'' increasing rows and ''k'' increasing columns on which ''A'' agrees with ''H'', zeros as well as ones. Must every ''A'' that needs at least ''εn''2 entry changes to become free of such copies contain at least ''c''''H''''ε''''C''''H''''n''2''k'' of them? A manuscript dated 25 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]) claims a negative answer. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* The manuscript's introduction traces the question to N. Alon, E. Fischer and I. Newman (SIAM J. Comput. 37 (2007), Section 7), and to Problem 1.4 of N. Alon and O. Ben-Eliezer, ''Efficient removal lemmas for matrices'' ([https://arxiv.org/abs/1609.04235 arXiv:1609.04235]). It states that the version for a single pattern is Conjecture 4.5 in the first arXiv version of the survey ''Polynomial property testing'' by L. Gishboliner and A. Shapira ([https://arxiv.org/abs/2508.16878v1 arXiv:2508.16878v1]).
* The manuscript also recalls that qualitative removal (a positive copy density for each fixed distance) is due to Alon, Ben-Eliezer and Fischer ([https://arxiv.org/abs/1704.02367 arXiv:1704.02367]), and that Alon and Ben-Eliezer proved polynomial bounds for finite families closed under row permutations.

== The original result ==
* '''Claim.''' There is a fixed binary 66×66 matrix ''H'' with the following property. For every ''h'' ≥ 1 put ''n''''h'' = (386''h'' + 2)2''h'' and ''ε''''h'' = (386''h'' + 2)−2. Then there is an ''n''''h''×''n''''h'' binary matrix that is ''ε''''h''-far from being ''H''-free yet has at most ''ε''''h''2−''h''''n''''h''132 ordered copies of ''H''. Hence no polynomial removal bound holds for this ''H''. Entry changes are allowed in both directions. The manuscript also derives a lower bound on the sample size of the canonical sampling tester that is exponential in a constant multiple of ''ε''−1/2.
* '''Source.''' [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026 Manuscript folder] in the openai/math repository (commit <code>1581d4c</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/190.md lean/docs/190.md] states that the formalization disproves a polynomial removal bound for one explicit 66×66 pattern. For every ''c'', ''C'' > 0 it gives a binary matrix at normalized edit distance at least some ''ε'' > 0 from being pattern-free, with fewer than ''cε''''C''''n''132 ordered copies. The construction gives an explicit sequence of such matrices, and edits are allowed in both directions.

== Public follow-up work ==
Each follow-up below replaces the 66×66 pattern by a smaller one, keeping the tree-based construction of the OpenAI manuscript. The pattern sizes are those stated by each source. None of them claims that its pattern is the smallest possible.
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
|-
| 2026-10-07 || ProveIt project, ''A 5×5 Obstruction to Polynomial Ordered Matrix Removal'', [https://github.com/VladimirReshetnikov/ProveIt/tree/bfbfe915186310fdf745a7a089e7dd88eeb773b1/Combinatorics/OrderedMatrices/Research/ordered-matrix-removal report folder] in VladimirReshetnikov/ProveIt || Extension || Replaces the anchor of the OpenAI construction by the 3×3 crown ''J''3 − ''I''3, giving a 5×5 obstruction. For hosts of order (20''h'' + 2)''m'' with ''m'' = 2''h'', the report determines exactly the number of copies (2''m''8), the least number of cells meeting all copies (''m'') and the least number of entry changes that remove all copies (''m''2). It also gives sampling thresholds. || A LaTeX research draft in a GitHub repository; its provenance record states that it was prepared with ChatGPT.
|-
| 2026-10-09 || Erebos Labs, [https://github.com/erebos-labs/ordered-matrix-removal-4x4 erebos-labs/ordered-matrix-removal-4x4], releases [https://github.com/erebos-labs/ordered-matrix-removal-4x4/releases/tag/v1.0.0 v1.0.0] and [https://github.com/erebos-labs/ordered-matrix-removal-4x4/releases/tag/v1.1.0 v1.1.0] || Extension (formalization) || The 4×4 pattern with rows 0110, 1001, 1010, 0111 admits no polynomial removal bound, with a Lean proof (v1.0.0). Release v1.1.0 adds that the host of order (14''h'' + 2)''m'' has edit distance exactly ''m''2. The v1.1.0 README states that the host, pattern, mode order and lower-bound strategy are inherited from the OpenAI collection, the ProveIt report and v1.0.0. || GitHub releases. The README states that the work and its audits were AI-assisted and that no human referee endorsement is claimed.
|-
| 2026-10-10 (last updated 2026-10-14) || Ryan Shea, [https://github.com/shea256/ordered-binary-matrix-removal shea256/ordered-binary-matrix-removal] || Extension (formalization) || Successive constructions in the repository end with a 3×4 obstruction (11 October) and the 3×3 pattern with rows 011, 101, 110 (12 October). This is the crown ''J''3 − ''I''3, and it admits no polynomial removal bound. The qualitative theorem is checked in Lean. The README states that the exact count of 7''m''4 copies for the host of the written proof is outside the Lean certificate. It also states that the tree, threshold entries, protected sampling and propagation come from the OpenAI construction. || A manuscript and Lean project in a GitHub repository, prepared with Codex assistance. The README states that a separate AI review of the written proof found no gap, that independent peer review is pending, and that no minimality or first-ever claim is made.
|-
| 2026-10-11 || Zinan Wang, [https://arxiv.org/abs/2610.15370 arXiv:2610.15370], ''A Four-by-Four Obstruction to Polynomial Removal for Ordered Binary Matrices''; repository [https://github.com/wzn1118/h4-ordered-matrix-removal wzn1118/h4-ordered-matrix-removal] || Extension (formalization) || The same 4×4 pattern as the Erebos Labs release, with a host of order (14''h'' + 2)''m'' having exactly 2''m''6 + (''m'' − 2)''m''5/2 copies and edit distance exactly ''m''2. The least number of cells meeting all original copies is exactly ''m''. The abstract states that the identities and the obstruction at every depth are formalized in Lean. The paper says that its tree-propagation mechanism follows the OpenAI manuscript. || arXiv preprint, version 1 (cs.DM), with the Lean sources as ancillary files.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Polynomial removal for ordered binary matrices - Revision history

Aftermath bot: New page: polynomial removal for ordered binary matrices (OpenAI 66x66 counterexample; public follow-ups by ProveIt, Erebos Labs, R. Shea and Z. Wang)