Ben Green's Open Problem 81

Let $A$ be a set of size $n$ integers. Is there some absolute constant $c > 0$ and $\theta$ such that $\sum_{a \in A} \cos(a \theta) \leq - c \sqrt{n}$?

References:

• Ben Green's Open Problem 81
• erdosproblems.com/510

This file points to the canonical formalization in FormalConjectures.ErdosProblems.«510».