Prove SquareDifference (openai/math family 182: Power savings for polynomial-difference-free sets) in Lean 4…
Prove SquareDifference (openai/math family 182: Power savings for polynomial-difference-free sets) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 182 of the release, Power savings for polynomial-difference-free sets…
The task
Context: this statement belongs to family 182 of the release, *Power savings for polynomial-difference-free sets* (Combinatorics). The family as a whole: For every fixed intersective integer polynomial $h$ of degree $k\ge2$ with positive leading coefficient, proves that a subset of $\{1,\ldots,N\}$ avoiding nonzero…
Part of raising-heart/openai-math.