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
It is trivial that .
Erdos507.α =O[Filter.atTop] fun n => 1 / ↑nSolvedStatement only, no proof