Planar distinct distances and unit-distance bounds

Proves almost every point in a large planar set sees nearly n distances, and lowers the unit-distance exponent 4/3.

2 papers September 23, 2026 Explained by AI

Put n points in the plane and stand at one of them. Erdős asked in 1957 whether some point always sees almost n different distances to the others. The first paper proves more: almost every point does. The second paper limits how many pairs can be exactly one unit apart, lowering a 1984 exponent of 4/3 by a fixed amount. A computer proof checker has formal versions of both main results.

First step

1946

Paul Erdős, distinct-distance and repeated-distance problems

Significance

Landmark

It resolves Erdős's weak pinned distance conjecture and gives the first fixed power saving over the 1984 unit-distance bound, both with Lean statements.

Trust

Formal proof listed

Field

Combinatorics

2 papers

The explanation

Take a 4 by 4 square grid of 16 points, one unit apart. Stand at a corner and measure the distance to each other point. The squared distances take 9 different values: 1, 2, 4, 5, 8, 9, 10, 13 and 18. Now stand at the point one step in from that corner, diagonally. From there you see only 5 different distances. Next count pairs of points exactly one unit apart. Each row has 3 such pairs, and so does each column, giving 24 pairs.

Erdős started both questions in 1946Source 1. The first asks how many distances a single point, called a pin, must see. The weak pinned conjecture says some point sees at least n^(1−ε) distances, for any small ε and large nSource 2. Erdős stated this in 1957Source 2. The best earlier pinned bound reached every exponent below about 0.864Source 3. Some points can see very few distances. For points on a circle plus its centre, the centre sees only oneSource 4.

The first paper proves the conjecture in a stronger form. For any fixed ε, all but a vanishing fraction of the n points see at least n^(1−ε) distancesSource 5. No assumption on spacing or position is needed, but the paper gives no rateSource 6. The obstacle is that distances are real numbers with no structure to count. The proof moves each set into a number field, a system of algebraic numbers, without changing any equality between distancesSource 7.

The second question asks for u(n), the largest number of unit-distance pairs among n points. For the grid above, 24 is well below 16^(4/3), about 40.3. Spencer, Szemerédi and Trotter proved u(n) is at most a constant times n^(4/3) in 1984Source 8. An OpenAI construction already showed u(n) can exceed n^(1+ε) for some sizesSource 9. The second paper shows u(n) is at most C·n^β for some fixed β below 4/3Source 10. Its proof combines incidence counting with entropy and heights of algebraic numbersSource 11.

How sure is this? Lean, a computer proof checker, has formal statements of both main theorems. So the papers prove them, as far as the Lean statements match the papers. The first paper gives no rate, and the second states no value for β. No specialist review of either paper is published.

What it doesn't show. This does not give explicit rates or constants. The first theorem has no rate of decay, and the second states no value for its new exponent. It also does not close the gap with the known lower bounds for unit distances.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Landmark if it holds up: it settles a named Erdős conjecture and improves a 1984 exponent, with Lean statements for both. Neither result has explicit constants, and no specialist review is published.

Words used

Pin: A chosen point from which distances to all other points are measured.
Distinct distances: The number of different lengths among a set of measured distances.
Unit distance: A pair of points exactly one unit apart.
Exponent: The power in a bound like n^(4/3), which says how fast it grows with n.
Number field: A number system built from the fractions by adding finitely many roots of polynomials.
Incidence: A point lying on a given curve, such as a circle.
Entropy: A measure of how much information a random choice carries.

The original papers (2)

The weak pinned planar distance theorem (PDF, opens in a new tab)
September 23, 2026 Formal proof listed
A power saving for planar unit distances (PDF, opens in a new tab)
September 23, 2026

Lean notes

All quoted lines (11)

Erd\Hos initiated the planar distinct-distance and repeated-distance problems in 1946.
The weak pinned planar distance theorem Back to text
Erd\Hos explicitly stated this question in 1957; the modern terminology appears, for example, in.
The weak pinned planar distance theorem Back to text
Katz and Tardos refined that method to obtain every exponent below $\frac{48-14e}{55-16e}=0.864137\ldots$ .
The weak pinned planar distance theorem Back to text
An exceptional set is necessary: if $P$ consists of points on a circle and its center, the center sees just one nonzero distance.
The weak pinned planar distance theorem Back to text
For every fixed $\varepsilon>0$ , all but $o(n)$ points of any $n$ -point planar set determine at least $n^{1-\varepsilon}$ distinct nonzero distances.
The weak pinned planar distance theorem Back to text
Its exponent $s$ is fixed; the theorem supplies no explicit rate of decay.
The weak pinned planar distance theorem Back to text
Transfer for real closed fields preserves every distance equality and disequality and puts each finite configuration in a number field.
The weak pinned planar distance theorem Back to text
Spencer, Szemer\'edi and Trotter established the upper bound $u(n)=O(n^{4/3})$ in 1984.
A power saving for planar unit distances Back to text
An OpenAI construction disproved it by giving at least $n^{1+\varepsilon}$ unit distances, for some fixed $\varepsilon>0$ , along an unbounded sequence of sizes.
A power saving for planar unit distances Back to text
There are absolute constants $0<C<\infty$ and $1\le\beta<4/3$ such that $u(n)\le Cn^\beta$ for every nonnegative integer $n$ .
A power saving for planar unit distances Back to text
The proof then combines these bounds with prediction and, at its last stage, algebraic independence and quadratic extensions.
A power saving for planar unit distances Back to text

Other sources

openai/math, Lean scope note for family 167 The formalization proves that there are absolute constants $C>0$ and $1\le\beta<4/3$ such that every finite planar point set of size $n$ determines at most $Cn^\beta$ unordered unit-distance pairs.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

166The higher-dimensional Erdős distinct-distances conjectureCombinatorics
171The hypercube Ramsey conjectureCombinatorics
160Superexponential van der Waerden numbersCombinatorics
159Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi boundsCombinatorics
181The Erdős–Gallai cycle-decomposition conjectureCombinatorics

Browse Combinatorics Erdős problems Distances and packing Open since the 1940s Lean-checked results Landmark results