Erdős Problem 872

Theorem 872 · Erdős

A trivial upper bound: a play can claim at most the $n - 1$ elements of $\{2, \dots, n\}$ , so $L(n) \leq n - 1$ .

Formal statement · Lean 4.lean

theorem erdos_872.trivial_upper_bound (n : ℕ) (hn : 2 ≤ n) :
    L n ≤ n - 1 := by
  sorry

Proof. sorry

Nobody has tried yet.