社区把 OpenAI Problem #190 反例从 66×66 缩到 3×4,Lean 验证通过

BorisMPower · x · 2026-10-12

Ryan Shea 等人发布对 OpenAI Problem #190（有序二值矩阵移除问题）反例的进一步改进：将禁止模式（forbidden pattern）从其此前的 4×4 缩小到 3×4（模式 1001/1010/0111），而 OpenAI 原始给出的反例是 66×66。该 3×4 模式被证明不存在多项式移除上界，完整定理已用 Lean 形式化验证（基于 OpenAI 的形式化基础），论文与代码已在 GitHub 开源，PR 已合并。构造显示对每个 h≥1，取 m=2^h、n=(14h+2)m，存在需要至少 m² 次编辑、但模式副本数不超过 2mn⁵ 的方阵宿主，从而对任意 c、C、ε₀ 都能满足修复成本 ≥εn² 而副本数 <cε^C n⁷。