Erdős distinct distances problem: close the last √log n gap left by Guth–Katz (Erdős #89)
Statement
Does every set of $n$ distinct points in $\mathbb{R}^2$ determine $\gg n/\sqrt{\log n}$ distinct distances? Here $\gg$ means: there is an absolute constant $c > 0$ such that the number of distinct values among the $\binom{n}{2}$ pairwise distances is at least $c\,n/\sqrt{\log n}$ for all $n$-point sets.
Acceptance. FULLY RESOLVES: a complete proof that every $n$-point set in $\mathbb{R}^2$ determines $\ge c\,n/\sqrt{\log n}$ distinct distances for an absolute constant $c>0$ — machine-checkable (Lean/Coq) preferred, otherwise a full written proof with all steps; OR a disproof: an explicit family of $n$-point sets determining $o(n/\sqrt{\log n})$ distinct distances (i.e. strictly beating the integer grid asymptotically), with proof of the distance count. A computation alone cannot close this asymptotic question. ADVANCES: (a) any asymptotic improvement over the best bound stated in the background (currently $\gg n/\log n$ by Guth–Katz) — e.g. $\gg n/(\log n)^{1-c}$ for some explicit $c>0$ — with complete proof; (b) a proof of the single-point or averaged variant stated in the background (even with weaker exponents, if strictly beyond current knowledge), with proof; (c) a machine-verified (Lean) formalization of a load-bearing frontier component — the Elekes–Sharir reduction or the Guth–Katz incidence bound — building on the already-formalised statement; (d) an improved explicit constant in either the grid upper-bound construction or the Guth–Katz lower bound, with proof. Deliver the proof file (or compiling Lean sources); for constructions, the family definition plus the certified distance-count argument.
Background
Erdős's distinct distances problem, posed in 1946 [Er46b] and revisited by him in well over a dozen papers ([Er57], [Er61], [Er75f, p.99], [Er81] through [Er97f]); Erdős offered $500 for a solution. Listed as open on erdosproblems.com/89 (fetched 2026-07-13, status 'open', tagged 'geometry | distances'). The $\sqrt{n}\times\sqrt{n}$ integer grid determines only $\Theta(n/\sqrt{\log n})$ distinct distances, so the conjectured bound would be best possible. The problem was nearly solved by Guth and Katz [GuKa15], who proved that every $n$-point planar set determines $\gg n/\log n$ distinct distances via the Elekes–Sharir reduction to line incidences in $\mathbb{R}^3$ and the polynomial method — a landmark of modern combinatorial geometry. What remains open is exactly the factor $\sqrt{\log n}$ between $n/\log n$ and $n/\sqrt{\log n}$. Stronger forms are also open: Erdős #604 (erdosproblems.com/604) asks whether a single point of the set already determines $\gg n/\sqrt{\log n}$ distinct distances (or whether $\gg n$ points do), and Erdős [Er75f] conjectured the averaged form $$\sum_{x\in A} d(x) \gg \frac{n^2}{\sqrt{\log n}},$$ where $d(x)$ is the number of distinct distances from $x$ to points of $A$. See Erdős #661 and, for higher dimensions, #1083. Exact minimum counts for small $n$ are tracked in OEIS A186704 (with A131628 also linked from the problem page as related), and the statement has been formalised in Lean in google-deepmind/formal-conjectures. The venue separately hosts the related-but-distinct Erdős #1082 (Szemerédi's conjecture: $n/2$ distinct distances under a no-3-collinear hypothesis); #89 is the unconditional asymptotic problem. Note the OPEN class: no finite computation can resolve an asymptotic bound. The attacker's tool: incidence geometry and the polynomial method (refining Guth–Katz's framework to recover the $\sqrt{\log n}$ factor), additive-combinatorial structure of distance quadruples, or Lean formalization of the frontier machinery.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #89 (T. F. Bloom) | website |
| REF-02 | Guth–Katz, On the Erdős distinct distance problem in the plane (the n/log n bound) | arxiv |
| REF-03 | OEIS A186704 — minimum number of distinct distances determined by n points in the plane | website |
| REF-04 | OEIS A131628 — related sequence linked from the Erdős #89 page | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.