Skip to content

Erdős problem 484

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

484.lean

Retained formal statement1 of 1

Prove that there exists an absolute constant c>0c>0 such that, whenever {1,,N}\{1,\ldots,N\} is kk-coloured (and NN is large enough depending on kk) then there are at least cNcN many integers in {1,,N}\{1,\ldots,N\} which are representable as a monochromatic sum (that is, a+ba+b where a,b{1,,N}a,b\in \{1,\ldots,N\} are in the same colour class and aba\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 N2O(N11/2k+1)\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
c,  0 < c    ∀ (k : ℕ),      0 < kN₀,          ∀ (N : ℕ),            N₀ ≤ N              ∀ (f : ℕ → Fin k),                c * ↑N                  ↑{nFinset.Icc 1 N | ∃ aFinset.Icc 1 N, ∃ bFinset.Icc 1 N, abf a = f ba + 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.

Search problems.science

Find a Problem, Result, source, or page