Community shrinks OpenAI Problem #190 obstruction from 66x66 to 3x4, verified in Lean
BorisMPower · x · 2026-10-12
Ryan Shea and collaborators published a further improvement to OpenAI Problem #190 (ordered binary matrix removal): a 3×4 forbidden pattern (1001/1010/0111), down from their previous 4×4 and OpenAI's original 66×66, with the full no-polynomial-removal-bound theorem verified in Lean on top of OpenAI's formalization. The explicit construction shows hosts requiring ≥m² arbitrary binary edits while having at most 2mn⁵ pattern copies. Paper and code are on GitHub; the PR is merged.
More from Research
- "Results Without Understanding" Is How LLMs Work—and Science Itself Is Changing — fkasummer · 2026-10-12
- The classic VAE tutorial that bridges deep learning and probabilistic modeling — goyal__pramod · 2026-10-12
- Anesthesia blocks consciousness via quantum microtubule effects, Stuart Hameroff argues ahead of Tucson conference — JosephJacks_ · 2026-10-12
- DeepMind's SynthID Bio protein watermarks now verifiable on Proteinbase — davidstutz92 · 2026-10-12
- Mathematicians push back on OpenAI's model-generated proofs — ZeeshanZiaML · 2026-10-12
- GaussiAnimate turns 4D captures into rigged 3D assets without physics simulation — janusch_patas · 2026-10-12