Erdős Problem 101

Reference: erdosproblems.com/101

noncomputable def Erdos101.numLinesWithFourPointMax (n : ℕ) : ℕ

The maximum number of lines containing exactly $4$ points among all sets $S$ of $n$ points in $\mathbb{R}^2$ satisfying the condition that no five points are collinear.

Equations

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

theorem Erdos101.erdos_101 : (fun (n : ℕ) => ↑(numLinesWithFourPointMax n)) =o[Filter.atTop] fun (n : ℕ) => ↑n ^ 2

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)$.