Power savings for planar halving lines and k-sets

1 paperLean

Improves the planar halving-line bound to \(O(n^{4/3-\varepsilon})\) for sets with no three collinear and an absolute ε > 0. More generally, an n-point set with no three collinear has \(O(n(k+1)^{1/3-\varepsilon_0})\) strictly separable k-subsets for \(1\le k\le n/2\), with an absolute \(\varepsilon_0\gt 0\). The constants and positive exponents are nonquantitative.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A power saving for planar halving lines

OpenAI · September 25, 2026

There are absolute constants ε > 0 and C such that every sufficiently large even n-point set in the plane with no three collinear has at most \(Cn^{4/3-\varepsilon}\) unordered halving pairs. This gives a power saving over the classical \(O(n^{4/3})\) bound for planar halving lines. The proof is nonquantitative and does not supply explicit constants.

Read PDF Download Source

Cite

@misc{OAI:A-power-saving-for-planar-halving-lines-September-25-2026,
  author = {{OpenAI}},
  title = {{A power saving for planar halving lines}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-power-saving-for-planar-halving-lines-September-25-2026/main.pdf}{OAI:A-power-saving-for-planar-halving-lines-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A power saving for planar halving lines

Scope

A halving pair in an even planar point set is a pair whose line leaves equally many remaining points on each side. The formalization proves that some absolute \(\varepsilon>0\) and \(C\) bound the number of halving pairs by \(Cn^{4/3-\varepsilon}\) for every sufficiently large even \(n\) and every \(n\)-point set with no three collinear. It also proves a bound of the same form for all level-switch counts under the additional generic-position assumptions in the statement. The constants are existential.

Comparator links

Result	Comparator statement
Power-saving bounds for halving pairs and level switches	HalvingLines.lean

Scope note on GitHub →