Skip to content

Erdős problem 282

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 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.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/282.lean

Formal Conjectures

FormalConjectures/ErdosProblems/282.leanErdos282.erdos_2821 lineExact file
∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Odd x.den → Erdos282.greedyUnitFractionRem {n | Odd n} x =ᶠ[Filter.atTop] 0
OpenStatement only, no proof

Continue