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
Resolved by Alon [Al91] who proved .
(fun n => ↑(Erdos798.t n)) =O[Filter.atTop] fun n => ↑n ^ (2 / 3) * Real.log ↑nSolvedStatement only, no proof