Erdős problem 194

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?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

194.lean

Retained formal statement1 of 1

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]. -

FormalConjectures/ErdosProblems/194.leanErdos194.erdos_1944 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.