ErdosProblems · research open · AMS 5

unsolvedsorry — nobody on it

Erdős Problem 282

Conjecture 282 · Erdős

Let A⊆NA\subseteq \mathbb{N} be an infinite set and consider the following greedy algorithm for a rational x∈(0,1)x\in (0,1): choose the minimal n∈An\in A not used so far such that n≥1/xn\geq 1/x and repeat with xx replaced by x−1nx-\frac{1}{n}. If this terminates after finitely many steps then this produces a representation of xx as the sum of distinct unit fractions with denominators from AA.

Does this process always terminate if xx has odd denominator and AA is the set of odd numbers?

Formal statement · Lean 4.lean
theorem erdos_282 {x : ℚ} (hx : x ∈ Set.Ioo 0 1) (hx_den : Odd x.den) :
    greedyUnitFractionRem { n | Odd n } x =ᶠ[atTop] 0 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗