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
Current best upper bound [CPZ24]: .
∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ Erdos507.α =O[Filter.atTop] fun n => Erdos507.upperBarrier n * ↑n ^ o nSolvedStatement only, no proof