Erdős Problem 484

Theorem 484 · Erdős

Prove that there exists an absolute constant $c>0$ such that, whenever $\{1,\ldots,N\}$ is $k$ -coloured (and $N$ is large enough depending on $k$ ) then there are at least $cN$ many integers in $\{1,\ldots,N\}$ which are representable as a monochromatic sum (that is, $a+b$ where $a,b\in \{1,\ldots,N\}$ are in the same colour class and $a\neq b$ ).

A conjecture of Roth. Solved by Erdős, Sárközy, and Sós [ESS89], who in fact prove that there are at least $\frac{N}{2}-O(N^{1-1/2^{k+1}})$ many even numbers which are of this form.

Formal statement · Lean 4.lean

theorem erdos_484 :
    ∃ c : ℝ, 0 < c ∧ ∀ k : ℕ, 0 < k → ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N → ∀ f : ℕ → Fin k,
      c * N ≤ (((Finset.Icc 1 N).filter fun n =>
        ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N,
          a ≠ b ∧ f a = f b ∧ a + b = n).card : ℝ) := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗