Erdős Problem 188

Reference: erdosproblems.com/188

def Erdos188.s : Set ℕ

The set of numbers $k$ such that $\mathbb{R}^2$ can be red/blue coloured with no pair of red points unit distance apart, and no $k$-term arithmetic progression of blue points with distance 1.

Equations

• Erdos188.s = {k : ℕ | ∃ (blue : Set ℂ), ((Set.univ \ blue).Pairwise fun (c₁ c₂ : ℂ) => dist c₁ c₂ ≠ 1) ∧ ¬∃ bs ⊆ blue, ∃ (s : ℂ), bs.IsAPOfLengthWith (↑k) s 1}

theorem Erdos188.erdos_188.nonempty : s.Nonempty

Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 14, 15):

It has been shown that there is a large $M$ so that it is possible to partition $\mathbb{E}^2$ into two sets $A$ and $B$ so that $A$ contains no pair of points with distance 1 and $B$ contains no A.P. of length $M$.

theorem Erdos188.erdos_188.estimate : (∀ k ∈ s, 5 ≤ k) ∧ ∃ k ∈ s, k ≤ 10000000

Old and new problems and results in combinatorial number theory by Erdős & Graham (Page 15):

How small can $M$ be made? The only estimate currently known is that $M$ ≤ 10000000 (more or less). In the other direction, it has just been shown by R. Juhász [Ju (79)] that we must have $M$ ≥ 5.

theorem Erdos188.erdos_188 : IsLeast s sorry

What is the smallest $k$ such that $\mathbb{R}^2$ can be red/blue coloured with no pair of red points unit distance apart, and no $k$-term arithmetic progression of blue points with distance 1?