Erdős #89 — distinct distances in the plane

Statement

Does every set of $n$ distinct points in $\mathbb{R}^2$ determine $\gg n/\sqrt{\log n}$ many distinct distances?

Equivalently: let $D(n) = \min_{|P|=n} D(P)$ where $D(P)$ is the number of distinct pairwise distances spanned by a planar point set $P$. Is $D(n) = \Omega(n/\sqrt{\log n})$?

Facts

- Prize $500; status per erdosproblems.com/89 (site-owner belief, verified by direct fetch 2026-07-02): OPEN, not finite — "This is open, and cannot be resolved with a finite computation." - Falsifiable: no — this is a lower-bound-for-all-$n$ statement; no finite point configuration can disprove it (a small-$n$ counterexample would only show the *constant* is wrong, not settle the $\Omega(\cdot)$ asymptotic), and no finite computation can prove it either. Needs a genuine proof. - Origin: #89 : [Er46b] [Er57] [Er61] [Er75f,p.99] [Er81] [Er82e] [Er83c] [Er85] [Er87b,p.170] [Er90] [Er92e] [Er95] [Er97b] [Er97c] [Er97e] [Er97f] [Va99,4.69]. [Er46b] = P. Erdős, "On sets of distances of $n$ points," Amer. Math. Monthly 53 (1946), 248–250 — the original paper (confirmed via the Lean file's reference list, raw.githubusercontent.com/google-deepmind/formal-conjectures/main/FormalConjectures/ErdosProblems/89.lean). - Tightness / why $\sqrt{\log n}$: a $\sqrt n \times \sqrt n$ section of the integer lattice $\mathbb{Z}^2$ determines $\Theta(n/\sqrt{\log n})$ distinct distances — this is the conjectured-optimal example, and it is *tight as a consequence of the Landau–Ramanujan theorem*: the number of positive integers $\leq n$ that are a sum of two squares is $\Theta(n/\sqrt{\log n})$, and every squared-distance in the grid is such a sum (Sheffer survey, arXiv:1406.1949, §1–2, citing Erdős's original observation). This is the mechanism, not just an example — it is the reason the exponent involves $\sqrt{\log n}$ at all. - Nearly solved by Guth & Katz [GuKa15] (L. Guth, N. H. Katz, "On the Erdős distinct distance problem in the plane," Annals of Math. 181(1) (2015), 155–190; arXiv:1011.4105), who proved the matching lower bound up to a $\sqrt{\log n}$ factor: $D(n) = \Omega(n/\log n)$. This is the sharp exponent (1, up to log factors) — only the *log-power* is still open, not the polynomial exponent. Read directly from the arXiv abstract + intro (verified 2026-07-02). - History of lower bounds before Guth-Katz, as stated in the Guth-Katz paper's own introduction (arXiv:1011.4105, p.1): Erdős 1946 gave $\Omega(n^{1/2})$; successive improvements by Moser [M], Chung–Szemerédi–Trotter [CSzT], Székely [Sz], Solymosi–Tóth [SoTo], Tardos [T], culminating in Katz & Tardos [KT] (2004) at $\Omega(n^{0.8641\ldots})$ via an entropy-inequality method — "the most recent lower bound... says the number of distances is $\gtrsim n^{.8641}$" (Guth-Katz, arXiv:1011.4105, p.1). - Method: Guth-Katz follow the Elekes–Sharir reduction (in the "spirit of the Erlangen program") converting the distance problem to a point-line incidence problem in the group $SE(2)$ of rigid motions of the plane, then introduce (a) a cell decomposition via the polynomial ham-sandwich theorem to control points with many incident lines, and (b) the flecnode polynomial (G. Salmon, 19th century) plus the geometry of ruled surfaces to control points with only two incident lines. This is the origin of the modern "polynomial method" in combinatorial geometry (also used for the finite-field Kakeya problem by Dvir). - Stronger, still-open forms (linked directly from erdosproblems.com/89's "See also"): - Erdős #604 — pinned distinct-distances at a single point — the pinned distance problem ($500 prize, also open): is there a *single* point $x \in A$ determining $\gg n/\sqrt{\log n}$ distinct distances (or even the weaker $\gg n^{1-o(1)}$)? This is strictly stronger than #89. Crucially, the Guth-Katz polynomial method has not been pushed through for the pinned version: the best known bound for #604 is still the older Katz–Tardos [KaTa04] entropy bound $\Omega(n^{c-o(1)})$, $c = \frac{48-14e}{55-16e} = 0.864137\ldots$ (erdosproblems.com/604, verified by direct fetch) — i.e. #89 is fully "nearly solved" but its natural strengthening #604 is stuck at the pre-2015 bound. This is a genuine open gap in the technique, not just in the statement. - Erdős #661 — bipartite distinct-distances o(n/√log n) question is OPEN ($50); the underlying two-set function D(m,n) is SOLVED up to a log factor (Elekes construction 1995/1999, matching lower bounds by Mathialagan 2019) — a bipartite/two-point-set variant (prize $50, open): can $n$ pairs $x_i, y_i$ realize $o(n/\sqrt{\log n})$ cross-distances? - Erdős #1083 — distinct distances in R^d (d≥3) is OPEN; the solved d=2 case (#89, Guth–Katz) is the literal numerical input to every known partial bound, via Solymosi–Vu's dimension-reduction recursion — the generalization to $\mathbb{R}^d$, $d \geq 3$: is $f_d(n) = n^{2/d - o(1)}$? Erdős [Er46b] proved $n^{1/d} \ll_d f_d(n) \ll_d n^{2/d}$; best known lower bound (Aronov–Pach–Sharir–Tardos [APST04]) is weaker than the conjectured exponent — the polynomial method has extended partial results here (Solymosi–Vu and others) but the full conjecture is open in every dimension $d\geq 3$ (erdosproblems.com/1083, verified by direct fetch). - Formalized: Yes — erdosproblems.com marks "Formalised statement? Yes." Confirmed directly: FormalConjectures/ErdosProblems/89.lean (google-deepmind/formal-conjectures) states erdos_89 (the full $n/\sqrt{\log n}$ conjecture, @[category research open], sorry), plus three already-*proved-in-the-literature* companion lemmas marked @[category research solved]: the Guth–Katz bound erdos_89.variants.n_dvd_log_n ($\Omega(n/\log n)$), the grid upper bound erdos_89.variants.grid_upper_bound ($O(n/\sqrt{\log n})$), and a trivial-implication sanity lemma — all still sorry'd (statements only, no machine proofs yet). - No AI involvement found: the github.com/teorth/erdosproblems wiki "AI contributions to Erdős problems" page (fetched in full, 678 lines, grepped for "89") does not mention #89, despite listing dozens of other problems (e.g. #868, #871, #897, #1089) advanced by GPT-5.x, Claude Opus, Gemini 3, or Aristotle in late 2025/2026. No published exponent-improving paper since 2015 was found in a 30-most-recent arXiv scan for "distinct distances plane" (2018–2026 hits: surface variants, hyperbolic-surface variants, positive-characteristic variants, angle-problem variants — none touching the core planar exponent). - Related problems: Erdős #604 — pinned distinct-distances at a single point (pinned/stronger form, $500), Erdős #661 — bipartite distinct-distances o(n/√log n) question is OPEN ($50); the underlying two-set function D(m,n) is SOLVED up to a log factor (Elekes construction 1995/1999, matching lower bounds by Mathialagan 2019) (bipartite variant, $50), Erdős #1083 — distinct distances in R^d (d≥3) is OPEN; the solved d=2 case (#89, Guth–Katz) is the literal numerical input to every known partial bound, via Solymosi–Vu's dimension-reduction recursion (higher-dimensional generalization, no prize listed on the page).

Literature state

Not resolved — genuinely open, but famously "nearly solved." Guth & Katz (2015, Annals of Math., arXiv:1011.4105) proved the sharp polynomial exponent $D(n) = \Omega(n/\log n)$, closing essentially the entire gap that had been open since 1946; only a factor of $\sqrt{\log n}$ separates the best known lower bound from the conjectured-tight upper bound witnessed by the integer lattice (whose optimality itself follows from the classical Landau–Ramanujan theorem on sums of two squares, arXiv:1406.1949 §1–2). This is widely regarded as one of the landmark results in combinatorial/incidence geometry of the last 20 years and is the origin event for the modern "polynomial method" (cell decomposition via polynomial ham-sandwich, algebraic/ruled-surface arguments) that has since been exported to many other incidence problems (Kakeya-type bounds, Zarankiewicz-type unbalanced incidence bounds — cf. arXiv:2412.10204, found in the recent-paper scan). No paper closing the remaining $\sqrt{\log n}$ gap, or disproving the conjecture, was found in an arXiv search through 2026-06. The problem is explicitly still listed "open" on erdosproblems.com (last updated per the site's own remarks, checked 2026-07-02) and in the teorth/erdosproblems community YAML (status: open, last_update 2025-08-31). No AI/LLM system is recorded as having engaged with #89 specifically (checked the community "AI contributions" wiki in full). The natural strengthening to a *pinned* version (#604, "some/every point sees $\gg n/\sqrt{\log n}$ distances") is a strictly harder open problem where the Guth-Katz polynomial-method breakthrough has not yet been transferred — #604's best bound is still the pre-2015 Katz–Tardos entropy bound $n^{0.8641\ldots}$, a concrete unclosed technique-gap. Formalized in Lean as a statement (google-deepmind/formal-conjectures) but entirely sorry'd, including the already-solved Guth-Katz sub-result — so no verified formal proof exists yet even for the *solved* $n/\log n$ bound, let alone the open $n/\sqrt{\log n}$ conjecture.

Attack surface

- Mode: literature-resolution (closed as far as the frontier goes — this needs a genuine new proof idea, not a finite search) + derivation (the concrete, well-defined target is *closing the $\sqrt{\log n}$ factor in the Guth-Katz argument*, or transferring the polynomial method to the pinned-distance form #604 to beat Katz-Tardos's $n^{0.8641}$). - Concrete first experiment: not finite-search-amenable for the main conjecture itself (falsifiability: not-finite). The one genuinely tractable finite-computation angle is on the *adjacent, falsifiable* Lean-formalization gap: (1) actually machine-verify the Guth-Katz $\Omega(n/\log n)$ *solved* sub-theorem in Lean (erdos_89.variants.n_dvd_log_n, currently sorry'd in google-deepmind/formal-conjectures) — this is "only" a formalization task on a fully known, published, correct proof, not new mathematics, but it is concrete, checkable, and currently unclaimed; (2) separately, computational exploration of whether *any* non-lattice near-optimal configuration ($D(P) = O(n/\sqrt{\log n})$) exists that isn't a transform of $L_r = \{(i, j\sqrt r): i,j\in\mathbb Z\}$-type rectangular lattices (Sheffer survey Problem 2/3, arXiv:1406.1949) — this attacks a companion *structural* open problem (characterizing near-optimal sets) rather than #89's asymptotic itself, but is finite-search-friendly and cited as "hardly anything is known" even 12 years post-Guth-Katz. - Oracle: for the main conjecture, none mechanical — it requires a proof. For the Lean-formalization sub-task, the oracle is the Lean kernel typechecker itself (fully mechanical, zero-trust verification of a sorry-free proof term). For the near-optimal-structure computational angle, the oracle is exact rational/algebraic arithmetic on candidate point sets plus exhaustive or ILP-based distinct-distance counting for small-to-moderate $n$, cross-validated against known near-optimal families. - Feasibility: honest read: famous and hard for the core $500 conjecture — this is a problem that took ~70 years and a genuinely novel technique (the polynomial method, a Fields-Medal-adjacent-level breakthrough) just to reach $\Omega(n/\log n)$; closing the remaining $\sqrt{\log n}$ is recognized by the field (Sheffer survey, "Problem 1... almost completely solved") as the hard residual kernel, not low-hanging fruit — not in reach for a bounded effort. Two lower-risk, concretely valuable adjacent contributions: (a) formalizing the already-published Guth-Katz proof in Lean (pure engineering effort against a sorry, no new math, directly fills a real, currently-empty gap in google-deepmind/formal-conjectures); (b) attacking Erdős #604 — pinned distinct-distances at a single point (pinned distances) specifically, since it is the one place where a "transfer the Guth-Katz polynomial method to a related-but-different incidence setup" derivation move has a concrete, well-defined, currently-unbeaten target ($n^{0.8641}$) rather than requiring a wholly new idea against the sharp exponent.

Related

- Erdős #604 — pinned distinct-distances at a single point — pinned distance problem, strictly stronger form of #89, still stuck at the pre-Guth-Katz Katz-Tardos bound $n^{0.8641}$; the natural next target for transferring the polynomial method - Erdős #661 — bipartite distinct-distances o(n/√log n) question is OPEN ($50); the underlying two-set function D(m,n) is SOLVED up to a log factor (Elekes construction 1995/1999, matching lower bounds by Mathialagan 2019) — bipartite/two-point-set distinct-distances variant, $50 prize, open - Erdős #1083 — distinct distances in R^d (d≥3) is OPEN; the solved d=2 case (#89, Guth–Katz) is the literal numerical input to every known partial bound, via Solymosi–Vu's dimension-reduction recursion — higher-dimensional generalization ($f_d(n) = n^{2/d-o(1)}$?), open for all $d \geq 3$ - Polynomial method / slice rank (Croot-Lev-Pach, Ellenberg-Gijswijt) — Guth-Katz's cell decomposition via the polynomial ham-sandwich theorem + algebraic/zero-set arguments; the technique that resolved #89 up to log factors and later exported to Kakeya-type and Zarankiewicz-type incidence bounds - Elekes–Sharir(–Guth–Katz) reduction: distinct distances → point-line incidences in SE(2) — the reduction of the planar distinct-distances problem to point-line incidences in the group $SE(2)$ of rigid motions, "in the spirit of the Erlangen program"; the setup Guth-Katz build on - Flecnode polynomial / ruled-surface geometry (G. Salmon) — G. Salmon's 19th-century algebraic tool, used by Guth-Katz to show most incidence-lines lie on a ruled surface - Incidence geometry: Szemerédi–Trotter theorem, the crossing lemma, and Zarankiewicz-type bounds — the broader field (Szemerédi–Trotter theorem, crossing lemma, unbalanced Zarankiewicz bounds) that both feeds into and was reshaped by this problem - Landau–Ramanujan theorem: the density of sums of two squares is $\\Theta(x/\\sqrt{\\log x})$ — number-theoretic fact ($\Theta(n/\sqrt{\log n})$ integers $\leq n$ are sums of two squares) explaining why the integer-lattice upper bound, and hence the conjectured exponent, involves $\sqrt{\log n}$ - Entropy-inequality method (Katz–Tardos): Shannon-entropy linear programming for the sums-and-entries / distinct-distances problem — Katz-Tardos's 2004 pre-polynomial-method technique, still the record holder for the pinned-distance problem #604 - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — the erdosproblems.com/GDM formal-conjectures Lean statement exists but is entirely sorry'd, including the already-published Guth-Katz sub-result