Let $k\ge 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?

AMS 5 · solved (literature)

theorem erdos_194 :
  answer(False) ↔ ∀ k ≥ 3, ∀ r : ℝ → ℝ → Prop, IsStrictTotalOrder ℝ r →
    ∃ s : List ℝ, s.IsAPOfLength k ∧ (s.Pairwise r ∨ s.Pairwise (flip r))