Combinatorics

Green77.green_77

Given

n

points in the unit disc, must there be a triangle of area at most

n^{-2+o(1)}

determined by them?

References

Ben Green's Open Problem 77

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ o, Filter.Tendsto o Filter.atTop (nhds 0) ∧ Erdos507.α =O[Filter.atTop] fun n => ↑n ^ (-2 + o n)

What you must prove

import FormalConjectures.GreensOpenProblems.«77»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green77.green_77" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/77.lean

Source type SHA-256: sha256:ab6ba97b85e3e5a17231c85dde2623f20be4d66977e4fad39685725e405733eb
Task id: fc-379fc029-green77-green-77-035c0ca4b0-formalized-v1
Task commitment: sha256:da53d055780117287ff21e4ad2dc536ea17e58685942767e0139852942fcfc9f

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.