Erdős Problem 659

Reference: erdosproblems.com/659

noncomputable def Erdos659.minimalDistinctDistancesSubsetOfSize (points : Set (EuclideanSpace ℝ (Fin 2))) (n : ℕ) : ℕ

The minimum number of distinct distances determined by any subset of points of size n.

Equations

• One or more equations did not get rendered due to their size.

theorem Erdos659.erdos_659 : (∃ (a : ℕ → Finset (EuclideanSpace ℝ (Fin 2))), ∀ (n : ℕ), (a n).card = n ∧ 3 ≤ minimalDistinctDistancesSubsetOfSize (↑(a n)) 4 ∧ (fun (n : ℕ) => ↑(EuclideanGeometry.distinctDistances (a n))) ≪ fun (n : ℕ) => ↑n / √(Real.log ↑n)) ↔ sorry

Is there a set of $n$ points in $\mathbb{R}^2$ such that every subset of $4$ points determines at least $3$ distances, yet the total number of distinct distances is $\ll \frac{n}{\sqrt{\log n}}$?