Erdős problem 282
Let be an infinite set and consider the following greedy algorithm for a rational : choose the minimal such that and repeat with replaced by . If this terminates after finitely many steps then this produces a representation of as the sum of distinct unit fractions with denominators from .
Sources
FormalConjectures/ErdosProblems/
282.lean
Retained formal statement
In 1202 Fibonacci observed that this process terminates for any when .
∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Erdos282.greedyUnitFractionRem Set.univ x =ᶠ[Filter.atTop] 0TextbookStatement only, no proof