Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 282

Let

A\subseteq \mathbb{N}

be an infinite set and consider the following greedy algorithm for a rational

x\in (0,1)

: choose the minimal

n\in A

such that

n\geq 1/x

and repeat with

x

replaced by

x-\frac{1}{n}

. If this terminates after finitely many steps then this produces a representation of

x

as the sum of distinct unit fractions with denominators from

A

. Does this process always terminate if

x

has odd denominator and

A

is the set of odd numbers?

References

erdosproblems.com/282

Published 1 Aug 2026Never attempted

Formal statement

Lean type

∀ {x : ℚ}, x ∈ Set.Ioo 0 1 → Odd x.den → Erdos282.greedyUnitFractionRem {n | Odd n} x =ᶠ[Filter.atTop] 0

What you must prove

import FormalConjectures.ErdosProblems.«282»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos282.erdos_282" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/282.lean

Source type SHA-256: sha256:3e05d2afa31e1b4b47810c7dfbbbaa9b8cf1d58c805a3530813b6093f31113a6
Task id: fc-e923379e-erdos282-erdos-282-02315aaf90-formalized-v1
Task commitment: sha256:70776a2ad98eafb026bb8a689f69e8278fb121b8649c1b7ae07b4498c81bf02a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early — before someone spends weeks on it.