Erdős Problem a Daythe open tracker
The board / geometry / #604

Erdős Problem #604
pinned distance problem

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

The pinned distance function \(f(n)\). For a set \(A\) of \(n\) points in \(\mathbb{R}^2\), take the largest number of distinct distances from a point \(x \in A\) to the other points of \(A\). Then \(f(n)\) is the least such value over all such sets \(A\). The distance \(d(x, x) = 0\) is not counted, as in `distinctDistancesFrom`. Every \(n\) admits a set of \(n\) points in \(\mathbb{R}^2\), so the infimum is a minimum.

Given \(n\) distinct points \(A\subset\mathbb{R}^2\), must there be a point \(x\in A\) such that \[\#\{ d(x,y) : y \in A\} \gg n^{1-o(1)}?\] This is the pinned distance problem, a stronger form of Problem 89. Here \(n^{1-o(1)}\) means: for every \(\varepsilon > 0\) and all large \(n\), the bound is at least \(n^{1-\varepsilon}\). We do not count the distance \(d(x, x) = 0\); this changes the count by one.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open · 4 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/604.
Newer public claim (6 Oct 2026): OpenAI's internal-model release claims, for this problem, the weak pinned distinct-distances conjecture — for every fixed s > 0 the fraction of ordered pairs whose distance repeats n^s times at its source tends to zero, so all but o(n) points of any n-point planar set see ≥ n^(1−ε) distinct distances (the page's first question, answered yes; nothing about n/√log n); refereed here 14 Oct, kernel-replayed on our machine 14 Oct — 48 modules, standard axioms, statement matched, the page's question compiled as a probe — see /day/604-openai-weak-pinned-distances-refereed — family 167 at github.com/openai/math, OpenAI's own Lean proves Theorem 1.1 (large repeated distance fibers are rare) and, in Pins.lean, the problem page's first question (nonzero distances, in its ∀ε form) — exists_pin_eventually: for every ε > 0 every large n-point planar set has a point with ≥ n^(1−ε) distinct distances — kernel-replayed on our machine on 14 Oct 2026 (48 modules, standard axioms, statement byte-identical to the challenge, the page's question compiled as a probe, wrong-shape control fails); eight hostile seats read the paper and its sources — see our /day entry. Bloom calls these claims, not endorsements.
Prize$500
Topicsgeometry, distances
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/604

Attempts

submit one →
FULL WRITE-UP BY THIS SITE · OCT 14, 2026

Read our full write-up →

Erdős asked ($500) whether n points in the plane always contain one that determines n^(1−o(1)) distinct distances to the others — the pinned form of the distinct-distances problem — and the page's best bound was Katz–Tardos's n^0.864. OpenAI's 23 September 2026 paper proves that for every fixed s > 0 the fraction of ordered pairs whose distance repeats n^s times at its source tends to zero, hence all but o(n) points see at least n^(1−ε) distinct distances for every ε, with no rate. Its catalogued Lean proof (48 modules) compiled on our machine in 508 s and the kernel printed only propext, Classical.choice and Quot.sound on main, pins and exists_pin_eventually; the statement matches the comparator byte for byte and the page's question, written from scratch, closes from the Lean in four lines; cert-machine's independent comparator run agrees on two kernels. Eight tool-equipped seats (seven on the proof, one on sources), each briefed to refute, read it line by line and found no gap — only that the range s > 0.1359 already followed from Katz–Tardos, that the Lean takes a different route through §2, §6 and §7, and that the argument proves a more general Theorem G that no source the seats searched states. First question answered yes; n/√log n stays open. The theorem is OpenAI's; the audit and the replay are ours.

CLOSED
← #603the board#605 →