Ben Green's Open Problem 77

Reference:

• Ben Green's Open Problem 77

theorem Green77.green_77 : sorry ↔ ∃ (o : ℕ → ℝ), Filter.Tendsto o Filter.atTop (nhds 0) ∧ Erdos507.α =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (-2 + o n)

Given $n$ points in the unit disc, must there be a triangle of area at most $n^{-2+o(1)}$ determined by them?