Erdős problem 507
Let be such that every set of points in the unit disk contains three points which determine a triangle of area at most . Estimate .
Sources
FormalConjectures/ErdosProblems/
507.lean
Retained formal statement
Erdős observed that .
(fun n => 1 / ↑n ^ 2) =O[Filter.atTop] Erdos507.αSolvedStatement only, no proof