Combinatorics

Erdős 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

No one has attempted this yet.

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-379fc029-erdos282-erdos-282-f6f4c79ebe-formalized-v1
Task commitment: sha256:8988253214f41db86a4b96963e52ab1f48046fbe6c4b23a0e426c7e1196a2af9

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.