Progression-free Ramsey sets

DefinitionErdős Problem 966: progression-free sets that are Ramsey for shorter progressions#✓fully proved

This is the statement that for all natural numbers \(k \ge 2\) and \(r \ge 2\) there is a set \(A\) of natural numbers that contains no arithmetic progression of \(k + 1\) distinct terms and such that for every colouring \(c\) of the natural numbers with \(r\) colours there are a subset \(t \subseteq A\) that is an arithmetic progression of \(k\) distinct terms and a colour \(i\) with \(c(x) = i\) for every \(x \in t\).

Only the colours of elements of \(A\) matter, so the colouring condition says that every colouring of \(A\) with \(r\) colours has a monochromatic progression of \(k\) distinct terms.

def progressionFreeRamseySet : Prop :=
  ∀ k r : ℕ, 2 ≤ k → 2 ≤ r → ∃ A : Set ℕ, A.IsAPOfLengthFree (k + 1) ∧
    ∀ c : ℕ → Fin r, ∃ t ⊆ A, t.IsAPOfLength k ∧ ∃ i : Fin r, ∀ x ∈ t, c x = i

Uses 2 · Used by 1

Statement usesSets that are arithmetic progressions · Progression-free sets

Used byErdős Problem 966 holds

TheoremErdős Problem 966 holds#●ready to prove

For all natural numbers \(k \ge 2\) and \(r \ge 2\) there is a set \(A\) of natural numbers that contains no arithmetic progression of \(k + 1\) distinct terms and such that for every colouring \(c\) of the natural numbers with \(r\) colours there are a subset \(t \subseteq A\) that is an arithmetic progression of \(k\) distinct terms and a colour \(i\) with \(c(x) = i\) for every \(x \in t\).

public theorem_wanted progressionFreeRamseySet_holds : progressionFreeRamseySet

Sources

• T. F. Bloom, Erdős Problems, Problem #966, https://www.erdosproblems.com/966 (status PROVED (LEAN)); resolution: formal proof linked from erdosproblems.com/966 (found with Aristotle, posted in the comment thread); P. Erdős, Problems and results in combinatorial number theory (1975), 295-310, reports that Spencer had shown that such a sequence exists, erdosproblems.com/966 status 'proved (Lean)'; formal proof cited by formal-conjectures, https://github.com/plby/lean-proofs/blob/main/src/v4.29.1/ErdosProblems/Erdos966.lean.

Uses 1

Statement usesErdős Problem 966: progression-free sets that are Ramsey for shorter progressions

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.