The halving lines problem
From OpenAI Aftermath
The halving lines problem asks for the largest number of halving lines of n points in the plane with no three collinear: lines through two of the points that leave equally many of the remaining points on each side. More generally it concerns the number of k-sets, subsets of k points that a line can cut off. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September 2026, claims the first improvement of the exponent 4/3 in the upper bound. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Lovász and Erdős, Lovász, Simmons and Straus established the O(n3/2) scale for halving lines and developed the rotating-line viewpoint. Pach, Steiger and Szemerédi improved the upper bound by an iterated-logarithm factor, and Dey proved O(n(k + 1)1/3) for k-sets, hence O(n4/3) for halving lines, using convex chains and graph crossings. Alonso, López and Rodrigo later improved a lower-order term while keeping the exponent 4/3.
- For lower bounds, Erdős, Lovász, Simmons and Straus constructed sets with Ω(n log n) halving lines; Tóth obtained n·eΩ(√log n), and Nivasch simplified the construction and improved its constant.
- Pinchasi developed a related approach through balanced cuts ordered by slope and planar measure concentration.
The original result
- Claim. Theorem 1.1 of A power saving for planar halving lines states that there are absolute constants ε > 0, C and n0 such that every set of an even number n ≥ n0 of points in the plane with no three collinear has at most Cn4/3−ε halving lines. The manuscript states that the proof is nonquantitative and gives no numerical value of ε or effective values of C and n0.
- Further claims. Theorem 1.2 gives a bound of the same form, uniform in the rank, for the number of switches of the k lowest points in a rotating sweep of a generic configuration. Corollary 1.3 bounds the number of k-sets of n points with no three collinear, and the complexity of the k-level of an arrangement of n lines, by C0n(k + 1)1/3−ε0. The manuscript states that it asserts no corresponding saving for pseudolines or line segments.
- Method, as described: the central estimate bounds the number of disjoint sweep intervals of large activity, for which the crossing argument gives the 4/3 scale, and proves a uniform little-o improvement of this packing bound; one fixed scale then gives a contracting recurrence. If the packing bound were nearly attained, limiting measures of vertices, edges and crossings in compact rank coordinates built from convex chains would be absolutely continuous in a suitable sense. Monotonicity of the coordinates and a rigidity lemma for three transverse families of sweep lines recover Euclidean control, and a spatial mass estimate for strips together with a count of marked points crossing a boundary contradicts the positive edge mass.
- Source (openai/math repository, commit
7ef5c0c): A power saving for planar halving lines, dated 25 September 2026. - Formalization, as described by the repository. The scope note lean/docs/183.md states that the formalization proves the bound Cn4/3−ε for halving pairs of every sufficiently large even point set with no three collinear, and a bound of the same form for all level-switch counts under the additional generic-position assumptions, with existential constants. It links the comparator statement HalvingLines.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 28 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Halving lines, rank sweeps, and planar k-sets, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the claimed power saving below Dey's exponent 4/3: balanced lines and separable subsets, rank sweeps, the passage from an improved packing bound to a power saving, rank coordinates and their geometric meaning, strip mass and boundary tokens, and the dependence on the rank in the k-set bound. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | Formal Conjectures pull request #6979 | Statement (proposed) | Proposes adding Theorem 1.1, the power saving for halving lines, to the repository, citing the manuscript pinned at commit adc7f12. The description reports that a bridge applies the collection's Lean theorem to the proposed statement with only the standard axioms, checked by native Lean kernel builds rather than a sandboxed Comparator run, and that the all-ranks and k-set conclusions are not included. |
Open pull request, approved by a reviewer on 11 October 2026 and not merged when checked on 28 October 2026; the description discloses AI assistance. |
| 2026-10-16 | AI Proved What?, episode 183 Below 4/3?, remade version of 24 October 2026 | Reading (exposition) | Video explainer of the claim that n points in the plane with no three collinear have at most C times n to the power 4/3 − ε halving lines for an absolute ε > 0, improving Dey's exponent 4/3, with bounds of the same type for the switches at every rank of a rotating sweep and for k-sets. The episode states that no value of ε is given, that the true maximum still lies between Tóth's construction and this bound, and that nothing is claimed for pseudolines, line segments or higher dimensions. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 31 pages, dated September 25, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: both theorems, formalized by OpenAI, not run by the site. The k-set corollary is not formalized. The page also states that, by the site's count, the formal proof takes 47 files and 18,237 lines excluding Mathlib, that the site found no unproved steps by search without rebuilding the proof, that OSVerify has not reviewed the paper and that the site has seen no expert review. |
| 2026-10-17 | A power saving for planar halving lines, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Thirteen lessons: halving lines and rank sweeps; chains, crossings and Dey's bound; from packing to a power saving; measures on compact metric spaces, rank coordinates and limiting measures; monotone functions of two variables, independent gradients and three transverse foliations; the zoom at a rank point, a spatial measure and boundary activity; and levels and k-sets. | The lessons state that they were written by Claude Opus 5.5 (Anthropic) in October 2026 and self-checked by the writing AI; the course lists its status as author self-checked. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
