Erdős problem 966 · problems.science

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

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/966.lean

Formal Conjectures

FormalConjectures/ErdosProblems/966.leanErdos966.erdos_9663 linesExact file

1True ↔2  ∀ (k r : ℕ),3    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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:966
PLBY Lean proofsErdosProblems.Erdos966

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI building on literature
Erdős AI contributions wiki · 25 Feb, 2026
Machine
Aristotle
Open the source record
construction
VibeMathed
Machine
Aristotle
Reported outcome
resolved
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science