Documentation

FormalConjectures.ErdosProblems.«194»

Erdős Problem 194 #

References:

theorem Erdos194.erdos_194 :
False k3, ∀ (r : Prop), IsStrictTotalOrder r∃ (s : List ), s.IsAPOfLength k (List.Pairwise r s List.Pairwise (flip r) s)

Let $k\geq 3$. Must any ordering of $\mathbb{R}$ contain a monotone $k$-term arithmetic progression, that is, some $x_1 <\cdots < x_k$ which forms an increasing or decreasing $k$-term arithmetic progression?

The answer is no, even for $k=3$, as shown by Ardal, Brown, and Jungić [ABJ11].