Erdős Problem 510

References:

• erdosproblems.com/510
• Ben Green's Open Problem 81
• [Ru04] Ruzsa, Imre Z., Negative values of cosine sums. Acta Arith. (2004), 179-186.
• [Be25c] B. Bedert, Polynomial bounds for the Chowla Cosine Problem. arXiv:2509.05260 (2025).

theorem Erdos510.erdos_510 : True ↔ ∃ (c : ℝ) (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (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}?$$

theorem Erdos510.erdos_510.variants.ruzsa : ∃ (c : ℝ) (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ (θ : ℝ), ∑ n ∈ A, Real.cos (↑n * θ) < -Real.exp (c * √(Real.log ↑N))

Ruzsa [Ru04] proved an upper bound of $-\exp(O(\sqrt{\log N})$.

theorem Erdos510.erdos_510.variants.bedert : ∃ (c : ℝ) (_ : 0 < c), ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), 0 ∉ A → A.card = N → ∃ (θ : ℝ), ∑ n ∈ A, Real.cos (↑n * θ) < -c * ↑N ^ (1 / 7)

Bedert [Be25c] proved an upper bound of $-c N^{1/7}$.