Skip to content

Erdős problem 966

Let k,r≥2k,r\geq 2. Does there exist a set A⊆NA\subseteq \mathbb{N} that contains no non-trivial arithmetic progression of length k+1k+1, yet in any rr-colouring of AA there must exist a monochromatic non-trivial arithmetic progression of length kk? Answered in the affirmative.

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

966.lean

Retained formal statement1 of 1

Let k,r≥2k,r\geq 2. Does there exist a set A⊆NA\subseteq \mathbb{N} that contains no non-trivial arithmetic progression of length k+1k+1, yet in any rr-colouring of AA there must exist a monochromatic non-trivial arithmetic progression of length kk?

Erdős [Er75b] reported that 'Spencer has recently shown that such a sequence exists', but gives no reference.

FormalConjectures/ErdosProblems/966.leanErdos966.erdos_9663 linesExact file
True ↔  ∀ (k r : ℕ),    2 ≤ k → 2 ≤ r → ∃ A, A.IsAPOfLengthFree (↑k + 1) ∧ ∀ (coloring : ↑A → Fin r), ContainsMonoAPofLength coloring k
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