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
∀ (n : ℕ), Erdos282.greedyUnitFractionRem Set.univ (1 / ↑n) 0 = 0TestStatement only, no proof