All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsCombinatorics

Erdős Problem 282

Let ANA\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 nAn\in A such that n1/xn\geq 1/x and repeat with xx replaced by x1nx-\frac{1}{n}. If this terminates after finitely many...

Mathematical statement

Let ANA\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 nAn\in A such that n1/xn\geq 1/x and repeat with xx replaced by x1nx-\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?

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_282

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_282 {x : } (hx : x  Set.Ioo 0 1) (hx_den : Odd x.den) :    greedyUnitFractionRem { n | Odd n } x =ᶠ[atTop] 0 := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References