Erdős problem 484
Prove that there exists an absolute constant such that, whenever is -coloured (and is large enough depending on ) then there are at least many integers in which are representable as a monochromatic sum (that is, where are in the same colour class and ).
Sources
FormalConjectures/ErdosProblems/
484.lean
Retained formal statement
Prove that there exists an absolute constant such that, whenever is -coloured (and is large enough depending on ) then there are at least many integers in which are representable as a monochromatic sum (that is, where are in the same colour class and ).
A conjecture of Roth. Solved by Erdős, Sárközy, and Sós [ESS89], who in fact prove that there are at least many even numbers which are of this form.
∃ c, 0 < c ∧ ∀ (k : ℕ), 0 < k → ∃ N₀, ∀ (N : ℕ), N₀ ≤ N → ∀ (f : ℕ → Fin k), c * ↑N ≤ ↑{n ∈ Finset.Icc 1 N | ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n}.card