Erdős problem 798
Let be the minimum number of points in such that the lines determined by these points cover all points in .
Sources
FormalConjectures/ErdosProblems/
798.lean
Retained formal statement
A problem of Erdős and Purdy, who proved .
(fun n => ↑n ^ (2 / 3)) =O[Filter.atTop] fun n => ↑(Erdos798.t n)SolvedStatement only, no proof