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 ).
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/484.lean∃ 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}.cardProof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:484 - PLBY Lean proofs
ErdosProblems.Erdos484
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine