Erdős Problem 659

Reference: erdosproblems.com/659

theorem Erdos659.erdos_659 : sorry ↔ ∃ (A : ℕ → Finset (EuclideanSpace ℝ (Fin 2))), (∀ (n : ℕ), (A n).card = n ∧ ∀ S ⊆ A n, S.card = 4 → 3 ≤ EuclideanGeometry.distinctDistances S) ∧ (fun (n : ℕ) => ↑(EuclideanGeometry.distinctDistances (A n))) =O[Filter.atTop] fun (n : ℕ) => ↑n / √(Real.log ↑n)

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}}$?