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 .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/282.lean∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Odd x.den → Erdos282.greedyUnitFractionRem {n | Odd n} x =ᶠ[Filter.atTop] 0OpenStatement only, no proof