A power saving over the Spencer-Szemerédi-Trotter n^(4/3) bound for planar unit distances (Erdős Problem 90)

Erdős problem #90 · erdosproblems.com/90

Let $u(n)$ be the largest number of pairs at distance exactly $1$ among $n$ points of the Euclidean plane. Erdős introduced the problem in 1946, showed $u(n)\ge n^{1+c/\log\log n}$ and conjectured $u(n)=n^{1+o(1)}$ (erdosproblems.com Problem 90). Spencer, Szemerédi and Trotter proved $u(n)=O(n^{4/3})$ in 1984, and no better exponent was known; Valtr's metric with $n^{4/3}$ unit pairs shows that an improvement must use a special feature of the Euclidean metric, as the problem record notes. In 2026 an OpenAI construction disproved Erdős's conjecture with $u(n)\ge n^{1+\varepsilon}$ for infinitely many $n$ (Sawin: exponent $1.0141$ ). Can the upper exponent $4/3$ be lowered by a fixed amount: is $u(n)=O(n^{4/3-\delta})$ for some absolute $\delta>0$ ?

Result: Proved(see note)
Status: Partial result
AI contribution: AI-discovered
Method: Argument
Field: Combinatorial geometry; unit distances and incidences
Posed by: Paul Erdős (problem, 1946); the 4/3 upper bound is due to Spencer, Szemerédi and Trotter (1984)
Year posed: 1946
Years open: 80y
Solved: 2026-09-23
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 38 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1: there are absolute constants $0<C<\infty$ and $1\le\beta<4/3$ such that every set of $n$ points in the Euclidean plane has at most $Cn^\beta$ unordered pairs at distance $1$ , for every $n$ . This is the first improvement of the 1984 exponent $4/3$ . It leaves a gap to the lower bound $n^{1.0141}$ (Sawin) from the 2026 disproof of Erdős's $n^{1+o(1)}$ conjecture, and $\delta=4/3-\beta$ is not made explicit. Not addressed: distinct distances, higher dimensions, or other norms (for Valtr's metric $4/3$ is sharp).

What the AI did

The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties, and the Re(s) > 11/12 zero-free region whose write-up was human-edited). The manuscripts are authored 'OpenAI' and name no human author. The principal manuscript is 'A power saving for planar unit distances' (September 23, 2026). It cites the earlier OpenAI construction disproving Erdős's n^(1+o(1)) conjecture and the human exposition by Alon et al.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the unit-distance problem as posed: it gives absolute $C$ and $1\le\beta<4/3$ with $u(n)\le Cn^\beta$ for all $n$ , a power saving with no explicit $\beta$ . Lean: lean/ComparatorChallenges/PlanarUnitDistances.json exists and its solution module OAI.Geometry.UnitDistances.Main is present at the pinned commit; the challenge is not in the formalization catalogue (formalization.yaml). The statement file was read here: theorem main asserts that there are $C,\beta$ with $0<C$ , $1\le\beta<4/3$ and $u(n)\le Cn^\beta$ for every $n$ , where $u(n)$ is the largest number of unordered pairs at Euclidean distance $1$ in an $n$ -point subset of the plane. That states the headline. Not rebuilt here. The proof combines random cuttings, entropy and prediction arguments with heights of algebraic numbers; the saving is non-effective.

A power saving over the Spencer-Szemerédi-Trotter n^(4/3) bound for planar unit distances (Erdős Problem 90)

What was actually shown

What the AI did

Verification

Sources

Discussion