Erdős Problem 282

Exercise 282 · Erdős

The formal statement below is all there is.

Formal statement · Lean 4.lean

theorem greedyUnitFractionRem_zero (n : ℕ) : greedyUnitFractionRem .univ (1 / n) 0 = 0 := by
  sorry

Proof. sorry

Nobody has tried yet.