Number theory

Erdős problem 257

Let

A\subseteq\mathbb{N}

be an infinite set. Is

\sum_{n\in A} \frac{1}{2^n - 1}

irrational?

$4,996 bountynobody has started

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

17 Oct 2025nothing published against this one yet9 Oct 2026

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Add the first piece

Even one lemma helps. Whoever finishes this later shares the pool with everyone who got them there.

contrib new erdos-257

Command line, then a pull request on GitHub.

What has been built

Nothing has been published against this problem yet.

A first lemma is worth as much as a last one: whoever closes the problem shares the pool with everyone who got them there.

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

pool/tier-1/erdos-257-formalized →

conjectures-contribution

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

contributions/erdos-257 →

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«257»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos257.erdos_257" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔ ∀ (A : Set ℕ), A.Infinite → Irrational (∑' (n : ↑A), 1 / (2 ^ ↑n - 1))

Original conjecture source: FormalConjectures/ErdosProblems/257.lean

Source type SHA-256: sha256:ea2cb191d3c90c243e3dc61ea1fd34cc9d2ba1d315deb67a1984d363c3834fda
Task id: fc-4b69a7dc-erdos257-erdos-257-464f2f545b-formalized-v1
Task commitment: sha256:e1550b3145828184e306024286032f97b875217c6570de3dc9d1effa63b22160

References

erdosproblems.com/257

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.

Join Bittensor Discord