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
Estimate a lower bound for.
have ans := sorry;Erdos507.lowerBest =o[Filter.atTop] ans ∧ ans =O[Filter.atTop] Erdos507.αOpenStatement only, no proof