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
Erdos282.greedyUnitFractionRem {n | IsSquare n} 1 0 = 0TestStatement only, no proof