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 a≠ba\neq b).

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/484.lean

Formal Conjectures

FormalConjectures/ErdosProblems/484.leanErdos484.erdos_48410 linesExact file
∃ 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
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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:484
  • PLBY Lean proofsErdosProblems.Erdos484

Reported activity

Reported by these sources. Not reviewed here.

Continue