Below 4/3?

The claim, in plain words

Scatter an even number of points in the plane, no three on a line. A halving line passes through two of the points and leaves the same number of the others on each side. Four points in convex position have two (the diagonals); a triangle with a point inside has three; points on a circle have exactly half as many halving lines as points. In our experiments, random points have about two thirds as many. How many can n points have at most?

As the paper recounts, Lovász (1971) and Erdős, Lovász, Simmons and Straus (1973) established an upper bound of order n^3/2 and built sets with about n log n halving lines. Pach, Steiger and Szemerédi saved an iterated-logarithm factor, and Dey (1998) proved O(n^4/3) using convex chains and the crossing lemma (many segments on few points force many crossings), together with O(n(k+1)^1/3) for k-sets, groups of k points that a line can cut off. From below, Tóth built sets with n·e^{c√log n} halving lines, and Nivasch improved the constant. A 2024 paper the preprint cites improved only a lower-order term. Our own search among small sets found 12 points with 18 halving lines (a lower bound, not a proven maximum; no three of the points are exactly on a line, though some nearly are).

Result 183 is one OpenAI preprint, A power saving for planar halving lines (31 pages, dated September 25, 2026). Its Theorem 1.1: “There exist absolute constants ε > 0, C < ∞, and n₀ such that, for every even n ≥ n₀ and every n-point set P ⊂ ℝ² with no three collinear, h(P) ≤ Cn^4/3−ε.” Theorem 1.2 gives the same kind of bound for the switches at every rank of a rotating sweep, for generic points (a slightly stronger general position), and Corollary 1.3 bounds the number of k-sets by C₀n(k+1)^1/3−ε₀.

What it doesn’t claim

A value of ε. “The proof is nonquantitative: it supplies neither a numerical value of ε nor effective values of C and n₀.” In the final step ε = log 2/(2 log q) for a fixed scale q that a compactness argument shows exists; the proof takes q ≥ 4, so its ε is at most 1/4. Nothing about the true maximum, which still lies between Tóth’s construction and Cn^4/3−ε. Nothing for pseudolines, line segments or higher dimensions. The fractions inside the proof, such as 32/17, are not the saving.

Where it stands

Posted as a preprint

OpenAI, 31 pages, dated September 25, 2026

Peer reviewed

Not yet

Checked in Lean

Both theorems, formalized by OpenAI; not run by us. The k-set corollary is not formalized.

Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization whose comparator statement contains both theorems exactly: the halving-line bound and the bound at every rank of the sweep. By our count the proof takes 47 files and 18,237 lines, excluding Mathlib (source); like the paper, it shows that ε exists without computing it. The k-set corollary is not formalized. We found no unproved steps by search; we have not rebuilt the proof. The paper is not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

1. A rotating sweep. Turn a direction and mark the lowest half of the points across it. Each time the marked half changes, the two points that trade places span a halving line. The paper counts these switches at every rank, because restricting part of the sweep to the points that move in it changes the rank.
2. Dey’s 4/3. In each batch of the sweep, every leaving point is joined to every joining point, and across batches these segments link up into convex chains and concave chains. A convex and a concave chain cross at most twice, while the crossing lemma says that many segments on few points force many crossings, which caps the number of batches that each swap a points at about (N/a)^4/3.
3. Never tight. If that count were nearly tight, for small batches in larger and larger sets, a limit of the measures of points, edges and crossings would exist, with a positive part of the activity spread out evenly in two coordinates. Monotone coordinates, three directions and three families of parallel lines make the zoomed-in rank coordinates a linear copy of the plane, where every active point lies in one of three thin parallel strips, except for at most two per token crossing the boundary; the strips are too thin, a contradiction.
4. Recurse. So at some fixed scale q, any sweep splits into at most ½q^4/3 sweeps on at most N/q points each, and repeating gives N^4/3−ε with ε = log 2/(2 log q).

The paper builds on Dey’s chains and crossings, the crossing lemma of Ajtai, Chvátal, Newborn and Szemerédi and of Leighton, and, for the k-set corollary, Matoušek’s shallow cuttings.

The numbers in the video

• Our exact counts: 2 halving lines for a convex quadrilateral, 3 for a triangle with a point inside, n/2 for points on a circle.
• Random points uniform in a square: about 0.67n halving lines on average for n = 1,000 (20 samples).
• Our local search: 3, 6, 9, 13, 18, 22 and 25 halving lines for 4, 6, …, 16 points (lower bounds only). The pictured 8- and 12-point sets were spread out for drawing without changing which pairs are halving; the 12-point set has no three points exactly on a line, though some nearly.
• ε = log 2/(2 log q) for sample values of q: 0.25 for q = 4, about 0.075 for q = 100.
• The Lean count: our count of the import closure.

Read the source

• A power saving for planar halving lines (PDF), 31 pages.
• The Lean scope note.
• The collection’s catalog, where this is result 183.

The paper

OpenAI groups related papers into one result; this one has a single paper.

• A power saving for planar halving lines

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.