Prove MatrixRemoval (openai/math family 190: Polynomial removal fails for ordered binary matrices) in Lean 4…
Prove MatrixRemoval (openai/math family 190: Polynomial removal fails for ordered binary matrices) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 190 of the release, Polynomial removal fails for ordered binary matrices…
The task
Context: this statement belongs to family 190 of the release, *Polynomial removal fails for ordered binary matrices* (Combinatorics). The family as a whole: Disproves polynomial ordered binary matrix removal with one fixed $66\times66$ zero–one pattern. Matrices can require many binary-entry changes to become…
Part of raising-heart/openai-math.