Erdős Problem 104

Conjecture 104 · Erdős

Given $n$ points in $\mathbb{R}^2$ the number of distinct unit circles containing at least three points is $o(n^2)$ .

Formal statement · Lean 4.lean

theorem erdos_104 :
    (fun n : ℕ => (maxUnitCircleCount n : ℝ)) =o[atTop] (fun n : ℕ => (n : ℝ) ^ 2) := by
  sorry

Proof. sorry

Nobody has tried yet.