Prove HalvingLines (openai/math family 183: Power savings for planar halving lines and $k$-sets) in Lean 4…
Prove HalvingLines (openai/math family 183: Power savings for planar halving lines and $k$-sets) in Lean 4…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 183 of the release, Power savings for planar halving lines and $k$-sets…
The task
Context: this statement belongs to family 183 of the release, *Power savings for planar halving lines and $k$-sets* (Combinatorics). The family as a whole: Improves the planar halving-line bound to $O(n^{4/3-\varepsilon})$ for sets with no three collinear and an absolute $\varepsilon>0$. More generally, an $n$-point…
Part of raising-heart/openai-math.