Unit distances in $\mathbb{R}^d$: estimate $f_d(n)$, the maximum number of unit-distance pairs (Erdős #1085)
Statement
Let $f_d(n)$ be minimal such that, in any set of $n$ points in $\mathbb{R}^d$ (no separation condition), there are at most $f_d(n)$ pairs of points at distance exactly $1$. Estimate $f_d(n)$. The most difficult cases are $d=2$ (the classical Erdős unit distance problem) and $d=3$; for odd $d\geq 5$ the second-order term is open.
Acceptance. FULLY RESOLVES any one of the open regimes, with a complete proof (machine-checkable Lean/Coq preferred, else a full written proof): (a) $d=2$: matching upper and lower bounds for $f_2(n)$ up to $n^{o(1)}$; (b) $d=3$: matching exponents for $f_3(n)$; (c) odd $d\geq 5$: determination of the $n^{4/3}$ second-order term up to $(1+o(1))$, or an exact formula. ADVANCES: (a) any proven bound strictly improving a bound stated in the background (e.g. a larger valid exponent in the $d=2$ lower bound, an upper bound below $n^{4/3}$ for $d=2$, either exponent for $d=3$, or narrowed constants for odd $d\geq 5$); (b) new exact values of the planar function beyond those recorded in OEIS A186705, delivered with exhaustive search code and a certificate that no $n$-point configuration achieves more unit distances (or resolution of a bounded open case such as $n=27$); (c) record unit-distance configurations for concrete $(d,n)$ strictly beating the counts stated in the background/OEIS, certified by explicit coordinates and exact verification. Deliver the proof file, or the enumeration/construction code plus coordinates, counts, and verification certificates.
Background
Posed in this general form by Erdős [Er75f, p.103]; listed as open on erdosproblems.com/1085 (fetched 2026-07-13, status 'open', tagged 'geometry | distances'). The frontier, per the source page (last edited 23 May 2026): for $d=2$ the best known bounds are $n^{1+c}<f_2(n)\ll n^{4/3}$ for some small constant $c>0$ — the upper bound is Spencer–Szemerédi–Trotter [SST84], and the lower bound (valid for infinitely many $n$), which improved Erdős's classical lattice bound $n^{1+c/\log\log n}$, is credited by the site to an internal model at OpenAI (2026; see erdosproblems.com/90, the planar unit distance problem proper). For $d=3$ the best known bounds are $n^{4/3}\log\log n\ll f_3(n)\ll n^{3/2}\beta(n)$ for a very slowly growing $\beta$, the lower bound by Erdős [Er60b], the upper by Clarkson–Edelsbrunner–Guibas–Sharir–Welzl [CEGSW90]. For $d\geq 4$ the leading term is settled: the Lenz construction (points on orthogonal circles) gives $f_d(n)\geq \frac{p-1}{2p}n^2-O(1)$ with $p=\lfloor d/2\rfloor$, matched via the Erdős–Stone theorem [Er60b] up to $o(n^2)$. Erdős [Er67e] determined $f_d(n)$ up to $O(1)$ for even $d\geq 4$; Brass [Br97] determined $f_4(n)$ exactly and Swanepoel [Sw09] did so for all even $d\geq 6$. For odd $d\geq 5$, Erdős and Pach [ErPa90] proved $\frac{p-1}{2p}n^2+c_1n^{4/3}\leq f_d(n)\leq \frac{p-1}{2p}n^2+c_2n^{4/3}$ for constants $c_1(d),c_2(d)>0$, leaving the $n^{4/3}$-term constant open. Exact planar values are OEIS A186705, known for $n\leq 21$ ($0,1,3,5,7,9,12,\ldots,57$), with only bounds known at e.g. $n=27$ (Alexeev–Mixon–Parshall). A Lean formalisation of the statement exists in the formal-conjectures repository. The venue's finite-field unit-distance problem (max unit distances in $\mathbb{F}_p^2$) is a related but distinct analog. The attacker's tool: exhaustive enumeration of candidate unit-distance-maximal graphs plus realizability certification to extend the exact values of A186705; explicit record constructions for concrete $n$ (coordinates + exact arithmetic); and incidence-geometry arguments for the asymptotic exponents.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #1085 (T. F. Bloom) | website |
| REF-02 | OEIS A186705 — maximum number of occurrences of the same distance among n points in the plane | website |
| REF-03 | Lean formalisation of Erdős #1085 (google-deepmind/formal-conjectures) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.