Erdős problem 847
Let be an infinite set for which there exists some such that in any subset of of size there is a subset of size at least which contains no three-term arithmetic progression.
Sources
FormalConjectures/ErdosProblems/
847.lean
Let be an infinite set for which there exists some such that in any subset of of size there is a subset of size at least which contains no three-term arithmetic progression.
Is it true that is the union of a finite number of sets which contain no three-term arithmetic progression?
A negative answer was given by Reiher, Rödl, and Sales [RRS24], who proved that, for any , there exists such that every finite colouring of contains a three-term arithmetic progression, and yet every subset of of size contains a subset of size without a three-term arithmetic progression.
False ↔ ∀ (A : Set ℕ), Infinite ↑A → Erdos847.HasFew3APs A → ∃ n S, (∀ (i : Fin n), ThreeAPFree (S i)) ∧ A = ⋃ i, S i