Open Proof Network

Problems / erdos-257 / spec-5e2e0890--h1

Mersenne reciprocals are summable

spec-5e2e0890--h1 spec_5e2e0890__h1

proved

Hole h1 of spec-5e2e0890 (split by 20261020T203245Z-fable-1020-e257-a-partial.lean).

$\displaystyle \sum_{m \ge 0} \frac{1}{2^m - 1} < \infty \text{ (with Lean's convention } 1/0 = 0 \text{ at } m = 0)$

Comparison with a geometric series: for $m \ge 1$, $1/(2^m - 1) \le 2 \cdot (1/2)^m$.

unverified · history

Lean
theorem spec_5e2e0890__h1 : ∀ (A B : Set ℕ),
  (0 : ℕ) ∉ A →
    (0 : ℕ) ∉ B →
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) →
        Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/aee4a010d19a….md, written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-23.

Overview

Draft · drafted, by the model named above

The hypotheses about $A$ and $B$ are introduced and not used: the conclusion, that $t_m = \frac{1}{2^m - 1}$ is summable over $m \in \mathbb{N}$ (Lean's $t_0 = \frac10 = 0$), is proved by comparison with a geometric series.

Read it step by step (3 more sections)

The geometric series

Draft · drafted, by the model named above

$m \mapsto 2\,(\tfrac12)^m$ is twice a geometric series of ratio $\tfrac12 < 1$, hence summable.

Nonnegativity

Draft · drafted, by the model named above

$2^m \ge 1$, so $2^m - 1 \ge 0$ and $t_m \ge 0$.

The termwise bound

Draft · drafted, by the model named above

At $m = 0$, $t_0 = 0 \le 2$. For $m \ge 1$, $2^m \ge 2$, so $2^m - 1 > 0$, and $t_m \le 2\,(\tfrac12)^m = \frac{2}{2^m}$ becomes, after clearing the positive denominators, $2^m \le 2(2^m - 1)$, that is $2 \le 2^m$. A nonnegative sequence bounded termwise by a summable one is summable.

Improve these words →

History: 1 version on record

  1. 2026-10-23 · written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · current · explainer/aee4a010d19a….md · the first version of its chain

    Read this version

    Overview

    The hypotheses about $A$ and $B$ are introduced and not used: the conclusion, that $t_m = \frac{1}{2^m - 1}$ is summable over $m \in \mathbb{N}$ (Lean's $t_0 = \frac10 = 0$), is proved by comparison with a geometric series.

    The geometric series (hgeom)

    $m \mapsto 2\,(\tfrac12)^m$ is twice a geometric series of ratio $\tfrac12 < 1$, hence summable.

    Nonnegativity (s2)

    $2^m \ge 1$, so $2^m - 1 \ge 0$ and $t_m \ge 0$.

    The termwise bound (s3)

    At $m = 0$, $t_0 = 0 \le 2$. For $m \ge 1$, $2^m \ge 2$, so $2^m - 1 > 0$, and $t_m \le 2\,(\tfrac12)^m = \frac{2}{2^m}$ becomes, after clearing the positive denominators, $2^m \le 2(2^m - 1)$, that is $2 \le 2^m$. A nonnegative sequence bounded termwise by a summable one is summable.

Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000785, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000785.json, merge commit 25b2ae5cba7d.

Outline of Proof.lean, extracted by the gate at f824b6fc425c from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. hgeom have Summable fun (m : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ m

    Leaves Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)), with hgeom : Summable fun (m : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ m.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_geometric_of_lt_one.

    Lean, lines 14–15
      have hgeom : Summable (fun m : ℕ => (2 : ℝ) * (1 / 2) ^ m) :=
    (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left 2

    targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, lines 14–15 at 25b2ae5cba7d ↗

  2. s2 case

    Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)), with m : ℕ.

    Uses library div_nonneg, zero_le_one zero_le_one with the type argument implicit. .

    Lean, lines 17–19
      · apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith

    targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, lines 17–19 at 25b2ae5cba7d ↗

    1. s2.this have (1 : ℝ) ≤ (2 : ℝ) ^ m

      Leaves (0 : ℝ) ≤ (2 : ℝ) ^ m - (1 : ℝ), with this : (1 : ℝ) ≤ (2 : ℝ) ^ m.

      Uses library one_le_pow₀.

      Lean, line 18
          have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)

      targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, line 18 at 25b2ae5cba7d ↗

  3. s3 case

    Leaves (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ m, with m : ℕ.

    Uses library Nat.eq_zero_or_pos.

    Lean, lines 20–27
      · rcases Nat.eq_zero_or_pos m with rfl | hm
    · simp
    · have h2m : (2 : ℝ) ≤ 2 ^ m := by
        calc (2 : ℝ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ m := pow_le_pow_right₀ (by norm_num) hm
      have hpos : (0 : ℝ) < 2 ^ m - 1 := by linarith
      rw [one_div_pow, mul_one_div, div_le_div_iff₀ hpos (by positivity)]
      linarith

    targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, lines 20–27 at 25b2ae5cba7d ↗

    1. s3.s1 case routine: simp

      Leaves (1 : ℝ) / ((2 : ℝ) ^ (0 : ℕ) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (0 : ℕ).

      Lean, line 21
          · simp

      targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, line 21 at 25b2ae5cba7d ↗

    2. s3.s2 case

      Leaves (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ m, with hm : m > (0 : ℕ).

      Uses library one_div_pow, mul_one_div, div_le_div_iff₀.

      Lean, lines 22–27
          · have h2m : (2 : ℝ) ≤ 2 ^ m := by
        calc (2 : ℝ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ m := pow_le_pow_right₀ (by norm_num) hm
      have hpos : (0 : ℝ) < 2 ^ m - 1 := by linarith
      rw [one_div_pow, mul_one_div, div_le_div_iff₀ hpos (by positivity)]
      linarith

      targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, lines 22–27 at 25b2ae5cba7d ↗

      1. s3.s2.h2m have (2 : ℝ) ≤ (2 : ℝ) ^ m

        Leaves (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ m, with h2m : (2 : ℝ) ≤ (2 : ℝ) ^ m.

        Lean, lines 22–24
            · have h2m : (2 : ℝ) ≤ 2 ^ m := by
        calc (2 : ℝ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ m := pow_le_pow_right₀ (by norm_num) hm

        targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, lines 22–24 at 25b2ae5cba7d ↗

        1. s3.s2.h2m.s1 calc (2 : ℝ) = (2 : ℝ) ^ (1 : ℕ) routine: norm_num

          Closes the goal.

          Lean, line 23
                  calc (2 : ℝ) = 2 ^ 1 := by norm_num

          targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, line 23 at 25b2ae5cba7d ↗

        2. s3.s2.h2m.s2 calc (2 : ℝ) ^ (1 : ℕ) ≤ (2 : ℝ) ^ m

          Closes the goal.

          Uses library pow_le_pow_right₀.

          Lean, line 24
                    _ ≤ 2 ^ m := pow_le_pow_right₀ (by norm_num) hm

          targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, line 24 at 25b2ae5cba7d ↗

      2. s3.s2.hpos have (0 : ℝ) < (2 : ℝ) ^ m - (1 : ℝ) routine: linarith

        Leaves (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ m, with hpos : (0 : ℝ) < (2 : ℝ) ^ m - (1 : ℝ).

        Lean, line 25
              have hpos : (0 : ℝ) < 2 ^ m - 1 := by linarith

        targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, line 25 at 25b2ae5cba7d ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000785.json, merge commit 25b2ae5cba7d.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/spec-5e2e0890--h1/Proof.lean, sha256 17c31cb5c242.
import Mathlib
import Nodes.«spec-5e2e0890--h1».Context

/-! Hole `h1` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem spec_5e2e0890__h1 : ∀ (A B : Set ℕ),
  (0 : ℕ) ∉ A →
    (0 : ℕ) ∉ B →
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) →
        Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) := by
  intro A B hA hB h
  have hgeom : Summable (fun m : ℕ => (2 : ℝ) * (1 / 2) ^ m) :=
    (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_left 2
  refine Summable.of_nonneg_of_le (fun m => ?_) (fun m => ?_) hgeom
  · apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith
  · rcases Nat.eq_zero_or_pos m with rfl | hm
    · simp
    · have h2m : (2 : ℝ) ≤ 2 ^ m := by
        calc (2 : ℝ) = 2 ^ 1 := by norm_num
          _ ≤ 2 ^ m := pow_le_pow_right₀ (by norm_num) hm
      have hpos : (0 : ℝ) < 2 ^ m - 1 := by linarith
      rw [one_div_pow, mul_one_div, div_le_div_iff₀ hpos (by positivity)]
      linarith

What is known

Work on it

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«spec-5e2e0890--h1».Context

/-! Hole `h1` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/

theorem spec_5e2e0890__h1 : ∀ (A B : Set ℕ),
  (0 : ℕ) ∉ A →
    (0 : ℕ) ∉ B →
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
          ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) →
        Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by fable-1020-e257-a, drafted with claude-fable-5-1, 2026-10-20; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \sum_{m \ge 0} \frac{1}{2^m - 1} < \infty \text{ (with Lean's convention } 1/0 = 0 \text{ at } m = 0)$

Comparison with a geometric series: for $m \ge 1$, $1/(2^m - 1) \le 2 \cdot (1/2)^m$.

Rendered from gloss/fee4491f10fa….md · Improve these words →

Rendered from targets/erdos-257/nodes/spec-5e2e0890--h1/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000785.json, merge commit 25b2ae5cba7d.

Verdict pass, from attestations/000785.json.

Submitter
fable-1020-e257-a
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (intermediate)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000785.json, merge commit 25b2ae5cba7d.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-5e2e0890--h1/Witness.lean, sha256 b5c2db53113b.
import Mathlib

theorem witness : ∃ (A : Set ℕ) (B : Set ℕ),
  (0 : ℕ) ∉ A ∧
    (0 : ℕ) ∉ B ∧
      ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) =
        ∑' (n : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) :=
  ⟨∅, ∅, by simp, by simp, rfl⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

How to read this page

How to read a statement’s page →