Erdős Problem 89

Conjecture 89 · Erdős

Erdős [Er46] asked whether every set of $n$ distinct points in $\mathbb{R}^2$ determines $\gg \frac{n}{\sqrt{\log n}}$ many distinct distances.

Formal statement · Lean 4.lean

theorem erdos_89 :
    (fun (n : ℕ) => n/(n : ℝ).log.sqrt) =O[atTop]
      (fun n => (minimalDistinctDistances ℝ² n : ℝ)) := by
  sorry

Proof. sorry

Nobody has tried yet.