Combinatorics

On hold

Date added 5 Aug 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?

Withdrawn 6 Oct 2026

HOLD_STATEMENT_SOURCE_DISCREPANCY (the pinned greedy algorithm may reuse odd denominators, while upstream PR 5806 uses distinct denominators. Admission is suspended pending statement-correspondence review; the target is not solved and not retired. See HOLDS-2026-10-06.md.)

1 piece from 1 personlast one 2 months ago

week of 11 Nov 2025 · nothing publishedweek of 18 Nov 2025 · nothing publishedweek of 25 Nov 2025 · nothing publishedweek of 2 Dec 2025 · nothing publishedweek of 9 Dec 2025 · nothing publishedweek of 16 Dec 2025 · nothing publishedweek of 23 Dec 2025 · nothing publishedweek of 30 Dec 2025 · nothing publishedweek of 6 Jan 2026 · nothing publishedweek of 13 Jan 2026 · nothing publishedweek of 20 Jan 2026 · nothing publishedweek of 27 Jan 2026 · nothing publishedweek of 3 Feb 2026 · nothing publishedweek of 10 Feb 2026 · nothing publishedweek of 17 Feb 2026 · nothing publishedweek of 24 Feb 2026 · nothing publishedweek of 3 Mar 2026 · nothing publishedweek of 10 Mar 2026 · nothing publishedweek of 17 Mar 2026 · nothing publishedweek of 24 Mar 2026 · nothing publishedweek of 31 Mar 2026 · nothing publishedweek of 7 Apr 2026 · nothing publishedweek of 14 Apr 2026 · nothing publishedweek of 21 Apr 2026 · nothing publishedweek of 28 Apr 2026 · nothing publishedweek of 5 May 2026 · nothing publishedweek of 12 May 2026 · nothing publishedweek of 19 May 2026 · nothing publishedweek of 26 May 2026 · nothing publishedweek of 2 Jun 2026 · nothing publishedweek of 9 Jun 2026 · nothing publishedweek of 16 Jun 2026 · nothing publishedweek of 23 Jun 2026 · nothing publishedweek of 30 Jun 2026 · nothing publishedweek of 7 Jul 2026 · nothing publishedweek of 14 Jul 2026 · nothing publishedweek of 21 Jul 2026 · nothing publishedweek of 28 Jul 2026 · nothing publishedweek of 4 Aug 2026 · nothing publishedweek of 11 Aug 2026 · nothing publishedweek of 18 Aug 2026 · nothing publishedweek of 25 Aug 2026 · nothing publishedweek of 1 Sept 2026 · 1 piece publishedweek of 8 Sept 2026 · nothing publishedweek of 15 Sept 2026 · nothing publishedweek of 22 Sept 2026 · nothing publishedweek of 29 Sept 2026 · nothing publishedweek of 6 Oct 2026 · nothing publishedweek of 13 Oct 2026 · nothing publishedweek of 20 Oct 2026 · nothing publishedweek of 27 Oct 2026 · nothing publishedweek of 3 Nov 2026 · nothing published

11 Nov 2025a year of work on this problem3 Nov 2026

This target is on hold.

Admission is suspended while a statement, source or resolution claim is checked. It returns once that is resolved and the target is audited again.

What has been built

1 piece · 12 lemmas

1 Sept 2026
- The Fibonacci-Sylvester greedy expansion terminates
  5FqLp5…FfZZiK · 12 lemmas

Where this lives

conjectures-contribution

Every published piece for this problem, with its Lean source and its signed record.

contributions/erdos-282 →

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«282»
import TaskSupport

namespace Bounty

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

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

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

Original conjecture source: FormalConjectures/ErdosProblems/282.lean

Task id: fc-6a786f99-erdos282-erdos-282-02f097749a-formalized-v1
Task commitment: sha256:703b3732ee49cf9bb4018ba21b9a869e817f7480af322d38c3b0a83d465c3d4d

References

erdosproblems.com/282

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord