Erdős Problem 101

Conjecture 101 · Erdős

Given $n$ points in $\mathbb{R}^2$ , no five of which are on a line, the number of lines containing four points is $o(n^2)$ .

Formal statement · Lean 4.lean

theorem erdos_101 : (fun n => (numLinesWithFourPointMax n : ℝ)) =o[atTop] (fun n => (n : ℝ)^2) := by
  sorry

Proof. sorry

Nobody has tried yet.