Erdős problem 507

Let $\alpha(n)$ be such that every set of $n$ points in the unit disk contains three points which determine a triangle of area at most $\alpha(n)$ . Estimate $\alpha(n)$ .

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

507.lean

Retained formal statement6 of 7

Current best upper bound [CPZ24]: $\alpha(n) \ll n^{-7/6 + o(1)}$ .

FormalConjectures/ErdosProblems/507.leanErdos507.erdos_507.variants.upper_cpz241 lineExact file

1∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ Erdos507.α =O[Filter.atTop] fun n => Erdos507.upperBarrier n * ↑n ^ o n

SolvedStatement only, no proof