Erdős problem 484

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$ ).

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

484.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/484.leanErdos484.erdos_48410 linesExact file

1∃ c,2  0 < c ∧3    ∀ (k : ℕ),4      0 < k →5        ∃ N₀,6          ∀ (N : ℕ),7            N₀ ≤ N →8              ∀ (f : ℕ → Fin k),9                c * ↑N ≤10                  ↑{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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.