Erdős Problem 194

Theorem 194 · Erdő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]. -

Formal statement · Lean 4.lean

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

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗