Polynomial removal for ordered binary matrices
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 εn2 entry changes to become free of such copies contain at least cHεCHn2k of them? A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (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 (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 (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 (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 nh = (386h + 2)2h and εh = (386h + 2)−2. Then there is an nh×nh binary matrix that is εh-far from being H-free yet has at most εh2−hnh132 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. Manuscript folder in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note 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εCn132 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.
| 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, report folder in VladimirReshetnikov/ProveIt | Extension | Replaces the anchor of the OpenAI construction by the 3×3 crown J3 − I3, giving a 5×5 obstruction. For hosts of order (20h + 2)m with m = 2h, the report determines exactly the number of copies (2m8), the least number of cells meeting all copies (m) and the least number of entry changes that remove all copies (m2). 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, erebos-labs/ordered-matrix-removal-4x4, releases v1.0.0 and 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 (14h + 2)m has edit distance exactly m2. 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, 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 J3 − I3, and it admits no polynomial removal bound. The qualitative theorem is checked in Lean. The README states that the exact count of 7m4 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, arXiv:2610.15370, A Four-by-Four Obstruction to Polynomial Removal for Ordered Binary Matrices; repository wzn1118/h4-ordered-matrix-removal | Extension (formalization) | The same 4×4 pattern as the Erebos Labs release, with a host of order (14h + 2)m having exactly 2m6 + (m − 2)m5/2 copies and edit distance exactly m2. 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.