Erdős Problem 510

Reference: erdosproblems.com/510

theorem Erdos510.erdos_510 : sorry ↔ ∃ (c : ℝ) (_ : 0 < c), ∀ N > 0, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ (θ : ℝ), ∑ n ∈ A, Real.cos (↑n * θ) < -c * √↑N

Chowla's cosine problem

If $A\subset \mathbb{N}$ is a finite set of positive integers of size $N > 0$ then is there some absolute constant $c>0$ and $\theta$ such that $$\sum_{n\in A}\cos(n\theta) < -cN^{1/2}?$$