Erdős problem 101 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

101.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/101.leanErdos101.erdos_1011 lineExact file

1(fun n => ↑(Erdos101.numLinesWithFourPointMax n)) =o[Filter.atTop] fun n => ↑n ^ 2

OpenStatement only, no proof