erdős #659
Is there a set of points in such that every subset of points determines at least distances, yet the total number of distinct distances is
Worked, still open.
geometry · solved · possible · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (1)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
A concrete example is a **truncated anisotropic lattice** (a “stretched grid”). Take [ P_m={(i,\sqrt2,j):0\le i,j\le m-1}\subset \mathbb Z\times \sqrt2,\mathbb Z, ] so (|P_m|=m^2). ([Erdős Problems][1])
candidate solution ↗formal
AMS 52 · solved (literature)
theorem erdos_659 : answer(True) ↔ ∃ A : ℕ → Finset ℝ²,
(∀ n, #(A n) = n ∧ ∀ S ⊆ A n, #S = 4 → 3 ≤ distinctDistances S) ∧
(fun n ↦ distinctDistances (A n)) ≪ fun n ↦ n / sqrt (log n)formal-conjectures/659.lean ↗links
Lund and Sheffer · paper
status
solved