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
More generally, for which pairs and does this process terminate?
∀ (x : ℚ) (A : Set ℕ), Erdos282.greedyUnitFractionRem A x =ᶠ[Filter.atTop] 0 ↔ (x, A) ∈ sorryOpenStatement only, no proof