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 an upper bound for.
have ans := sorry;Erdos507.α =O[Filter.atTop] ans ∧ ans =o[Filter.atTop] Erdos507.upperBarrierOpenStatement only, no proof