Let $f_{d} (n)$ be minimal such that, in any set of $n$ points in $R^{d}$ , there exist at most $f_{d} (n)$ pairs of points which distance $1$ apart. Estimate $f_{d} (n)$ .

Worked, still open.

geometry · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

Let $U(P)$ be the number of pairs at distance $1$ in a finite set (P\subset\mathbb R^d). Your (f_d(n)) is exactly the extremal quantity [ f_d(n)=\max{U(P): P\subset\mathbb R^d,\ |P|=n}, ] i.e. the maximum possible number of unit distances among $n$ points.

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 52 · solved (literature)

theorem erdos_1085.variants.lower_d2 :
    ∃ c > (0 : ℝ), ∀ᶠ n : ℕ in atTop, (n : ℝ) ^ (1 + c / log (log n)) < f 2 n

formal-conjectures/1085.lean ↗

oeis

A186705 — The Erdős unit distance problem: the maximum number of occurrences of the same distance among n points in the plane.0,1,3,5,7,9,12,14,18,20,23,27,30,33,37,41,43,46,50,54,57

links

#90Does every set of

n

distinct points in

R^{2}

contain at most

n^{1 + O (1/ l o g l o g n)}

many pairs which are distance 1 apart?A186705

status