Episode 167, October 2026

Erdős distances, pinned down?

Two preprints claim that almost every point of a planar set sees nearly n distances, and that one distance can repeat at most a constant times n to a power below 4/3

Covers result 167 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

Play Episode 167: Erdős distances, pinned down? A 7 by 7 grid of points with one circle around its centre point for each of the nine distances it sees (our drawing).

6:53. English captions available. The video loads from YouTube when you press play.

Chapters

The claim, in plain words

Stand at one of n points in the plane and count the different distances to the others. In a 7 × 7 grid the centre sees only 9, because each circle around it passes through several points, while a corner sees 26; the centre of a circle of points sees just one. “Erdős initiated the planar distinct-distance and repeated-distance problems in 1946”, and in 1957 he asked whether some point must always see nearly n distances. As the pinned paper recounts, Solymosi and Tóth proved a pinned bound of order n^6/7, Tardos improved the exponent, and Katz and Tardos reached every exponent below 0.864137…. “These results guarantee one pin in every configuration.” The weak pinned conjecture asks for n^1−ε at some point, for every fixed ε > 0 and all large n. The second problem is how often one distance can repeat; by rescaling, how many pairs can be exactly 1 apart. Spencer, Szemerédi and Trotter proved at most a constant times n^4/3 in 1984, and Székely gave a crossing-number proof using two facts: “two unit circles meet in at most two points, and two points belong to at most two unit circles.” The unit-distance paper cites 2026 constructions, which we could not check, that disprove Erdős’s conjecture of n^1+o(1), reaching n^1.014114 for infinitely many sizes.

Result 167 rests on two OpenAI preprints, both dated September 23, 2026, which do not cite each other. The weak pinned planar distance theorem (27 pages), Theorem 1.1: “For every fixed s > 0, one has F_n(s) → 0 as n → ∞”, where F_n(s) is the largest fraction, over n-point planar sets, of ordered pairs (x, y) whose circle about x through y holds at least n^s points. Corollary 1.2: for every fixed ε > 0, all but a vanishing fraction of the points of any n-point planar set see at least n^1−ε distances, which resolves the weak pinned conjecture in a stronger form. A power saving for planar unit distances (53 pages), Theorem 1.1: “There are absolute constants 0 < C < ∞ and 1 ≤ β < 4/3 such that u(n) ≤ Cn^β for every nonnegative integer n.”

What they don’t claim

No numbers: the pinned theorem “supplies no explicit rate of decay”, and the unit-distance proof establishes “the existence of a fixed positive gap without estimating its size”. Not every point: “An exceptional set is necessary: if P consists of points on a circle and its center, the center sees just one nonzero distance.” Not the sharper pinned conjecture of order n/√log n at a point, the most a grid allows. Nothing new for the total number of distances, where Guth and Katz’s bound of order n/log n stands. Nothing about the true unit-distance exponent between the cited constructions and the new β. As our own illustration, grids fall further behind n^4/3 as they grow: scaled so their most common distance is 1, the 10 × 10 grid has 288 unit pairs (n^4/3 ≈ 464) and the 1000 × 1000 grid 25,992,416 (n^4/3 = 10⁸).

Where it stands

Posted as preprints: OpenAI, 27 and 53 pages, both dated September 23, 2026
Peer reviewed: Not yet; OSVerify reported one major issue in the unit-distance paper, with a proposed repair
Checked in Lean: Both main theorems formalized by OpenAI; not run by us

Last checked October 19, 2026. Neither preprint has been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization with comparator statements matching both main theorems exactly (pinned, unit distances). By our count the proofs take 47 files and 15,657 lines and 40 files and 28,113 lines, excluding Mathlib (pinned development, unit-distance development), with no unproved steps by our search; we have not rebuilt them. The almost-every-point corollary is proved in a further file, Pins.lean, that the catalog does not link. The Lean scope note says the unit-distance theorem “is not included” and then describes its formalization, and the repository’s formalization list omits the unit-distance paper. OSVerify, a Stanford review project, refereed the unit-distance paper and reported one major issue. The last sentence of Section 8.2 (p.46) says that a point generic over the coefficient field stays generic after the other grid points are adjoined; the grid lemma gives independence only over the base field, and OSVerify gives a counterexample over a larger field. It does not say the main theorem is false: the later arguments use only the correct, weaker form, and it proposes restricting the claim to the base field. An expert comment on its page says the issue and the fix are both correct, calling the sentence “false as stated, but this error is fixable.” No response from the authors is posted. A Lean proof that checks would settle the theorem whatever the paper’s write-up, but we have not run it. We have seen no other expert review.

How the proofs go

Pinned: two coordinates. Assume a fixed fraction of pairs sit on crowded circles, and make the coordinates algebraic by a transfer principle that keeps every distance equality. With z = x + iy and w = x − iy, the squared distance is (z_q − z_p)(w_q − w_p), so on a circle about a point, w is a Möbius function of z.
Pinned: arithmetic and random grids. The product formula balances the sizes of algebraic numbers over all absolute values. Points are grouped by closeness at each one, using randomly shifted and rotated nested square grids at the complex places, whose error has the same law for every pair (Lemma 3.1); a cell with more than half the points is replaced by its complement. Summed over all levels and absolute values, the overlap of two points is a constant plus a part for each point, “the main use of arithmetic in the proof”.
Pinned: two cases. The identity forces points on crowded circles to spread over the cells like the whole set. If the total scale grows, the cells form trees, and an elementary tree bound contradicts the identity; if it stays bounded, a limit would need Möbius maps carrying one non-atomic law onto another, which Lemma 7.1 rules out.
Unit distances: incidences and information. From sets with nearly n^4/3 unit pairs, points and unit circles form an incidence graph; random cuttings and Székely’s bound isolate a piece with controlled degrees, where two neighbours of one centre share little information, so a point can be predicted from a short record of test answers.
Unit distances: heights and algebra. A unit step changes z by d and w by 1/d. If the variation of these steps over all absolute values stays bounded, a determinant rules out a predicted point that nearly satisfies three unit equations; if it grows, the paper extracts many pairs whose ratios have large height while certain products of ratios have small height. Square roots that must be independent then allow one sign to flip, a contradiction. That fails when points share a unit circle, so pairs on unit circles through very many points are removed first.

The numbers in the video

Our pinned counts: in the 7 × 7 grid the centre sees 9 distances and a corner 26; in the 400 × 400 grid, from 13,787 to 51,347.
Our circle and centre: with 12 points on the circle, the centre sees 1 distance and each rim point 6.
Our unit pairs in grids scaled so the most common distance is 1: 288 for 100 points (n^4/3 ≈ 464), 98,176 for 10,000 (≈ 215,443), 25,992,416 for a million (10⁸).
Our small sets: the hexagon with its centre has 7 points and 12 unit pairs.
Our circle check: on the circle of radius 5 about the origin, all 12 grid points satisfy w = 25/z.
Our simulation of random nested grids: the average error is −1.457, −1.460 and −1.454 for pairs at distances 0.001, 1 and 50,000.
Our check of the unit-distance paper’s excluded case: with L = −b(ζ − 1)²/ζ, at b = 1 the quantity L(L − 4) is the perfect square ((ζ² − 1)/ζ)².

Read the source

The weak pinned planar distance theorem (PDF), 27 pages.
A power saving for planar unit distances (PDF), 53 pages.
The Lean scope note.
The collection’s catalog, where this is result 167.

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

The weak pinned planar distance theorem main paper
A power saving for planar unit distances companion

Transcript

Read the full script

0:00The problems

Put n points in the plane, stand at one of them, and measure the distance to every other point. How many different distances do you see? Erdős raised this pinned version of his distance problem in 1957. In a 7 by 7 grid, the centre sees only 9 distances, because each circle around it passes through several points, while a corner sees 26. And one point can see a single distance: put points on a circle and add its centre. So the question is whether some point always sees many. The best earlier results each guaranteed one such point: Solymosi and Tóth reached n^(6/7), and Katz and Tardos pushed the exponent to about 0.864. The weak pinned conjecture asks for n^(1−ε), for every fixed ε, once n is large. The second problem asks how often a single distance can repeat. Rescaling turns any distance into distance one, so count the pairs at distance exactly one. Scale our 10 by 10 grid so its most common distance, √5, becomes one, and 100 points give 288 unit pairs. In 1984, Spencer, Szemerédi and Trotter proved at most a constant times n^(4/3). Székely later gave a short crossing-number proof needing just two facts: two unit circles meet in at most two points, and two points lie on at most two unit circles. Grids fall further behind n^(4/3) as they grow. Erdős’s lattice construction gives a little more than n, and he conjectured n^(1+o(1)); the paper cites 2026 constructions, which we could not check, that disprove this, reaching about n^1.014 for infinitely many sizes. Later work improved the constant in the upper bound; the question was whether the exponent 4/3 itself could be lowered.

1:53The claims

Result 167 is two OpenAI preprints, both dated September 23. The first, 27 pages long, claims the weak pinned conjecture in a stronger form: for every fixed ε, all but a vanishing fraction of the points of any planar set of n points see at least n^(1−ε) distances. Its main theorem says that if you pick an ordered pair of points at random, the chance that the circle about the first point through the second holds at least n^s points tends to zero, for every fixed positive s, uniformly over all sets. The second preprint, 53 pages long, claims a power saving: there are constants C and β, with β below 4/3, such that n points never have more than C times n^β unit pairs. Neither paper gives a number. There is no rate for the vanishing fraction, and no value of β, only that it is below 4/3. Not every point is claimed; the centre of a circle shows why. Seeing on the order of n/√(log n) distances at one point, the most a grid allows, is a sharper conjecture left open. Nothing changes for the total number of distances, where Guth and Katz’s bound stands. The two papers do not cite each other; they share a toolkit, not a lemma.

3:13How the proofs go

The pinned proof starts from a failure: sets where a fixed fraction of pairs sit on crowded circles. A transfer principle replaces the coordinates by algebraic numbers without changing any distance equality. Then it uses two coordinates, z = x + iy and w = x − iy. The squared distance is the change in z times the change in w, so on a circle about a point, w is a Möbius function of z; we checked this at all 12 grid points on a circle of radius 5. Algebraic numbers have a size at every absolute value, ordinary and p-adic, and the product formula balances these sizes. At each absolute value, the proof groups points by closeness, using randomly shifted and rotated nested square grids at the complex ones. Our simulation shows the grids’ error has the same average for pairs at very different distances, the property the proof needs. Summed over all levels and absolute values, the overlap of two points is a constant plus a part for each point. That additive identity forces the points on crowded circles to spread over the cells like the whole set. Then there are two cases. If the total scale grows, the cells form trees, and an elementary bound shows that distances in trees fluctuate more than the identity allows. If it stays bounded, a limit would need Möbius maps carrying one spread-out distribution onto another in a way the paper shows is impossible. The unit-distance proof also argues by contradiction, from sets with nearly n^(4/3) unit pairs. It treats them as points and unit circles, and uses random cuttings and Székely’s incidence bound to isolate a piece with controlled degrees. There, two points that are neighbours of one centre share little information, so a point can be predicted from a short record of test answers. In the same two coordinates, a unit step changes z by some number d and w by 1/d, and the proof measures how these changes vary across all absolute values. If that variation stays bounded, a determinant rules out a predicted point that nearly satisfies three unit equations. If it grows, the paper extracts many pairs of points whose ratios have large height, a measure of arithmetic complexity, while certain products of ratios have small height. The finish is algebraic: square roots that must be independent let one sign flip, a contradiction. That step fails when the points share a unit circle, so pairs on unit circles through very many points are removed first; we checked the identity behind that case.

5:52Where it stands

Both papers are preprints, not peer reviewed, and not revised. Both main theorems are stated in Lean, and OpenAI’s files contain proofs of about 16,000 and 28,000 lines, with no gaps we could find by search; we did not run the check. The almost-every-point consequence is proved in a further uncatalogued file. The Lean documentation contradicts itself on whether the unit-distance theorem is included; its formalization is there. OSVerify, a Stanford review project, refereed the unit-distance paper and reported one major issue. A Lean proof that checks would settle the theorem whatever the paper’s write-up, but we have not run it. If they hold, almost every point of a planar set sees nearly n distances, and one distance repeats at most a constant times n to a power below 4/3: the exponent drops by a fixed amount, of unknown size.

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.