Open Proof Network

Problems / erdos-257 / spec-a70fcca4--h3

the Mersenne reciprocal series converges

spec-a70fcca4--h3 spec_a70fcca4__h3

proved

Hole h3 of spec-a70fcca4 (split by 20261020T203100Z-fable-1020-e257-b-partial.lean).

Restated as hole h3 of spec-a70fcca4-v2 (split by 20261020T203100Z-fable-1020-e257-b-partial.lean).

$\displaystyle \sum_{n\ge 0} \frac{1}{2^n-1} < \infty$

(summable; the n = 0 term is Lean's 0.) Comparison with the geometric series: 1/(2^n-1) ≤ 2/2^n for n ≥ 1.

unverified · history

Lean
theorem spec_a70fcca4__h3 : Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (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/6d95dbfa2185….md, written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22.

Overview

Draft · drafted, by the model named above

Compare $t_n = \frac{1}{2^n-1}$ termwise with $2\,(\frac12)^n$, a summable geometric series, and use that a nonnegative sequence dominated by a summable one is summable. (Lean's $t_0 = \frac10 = 0$.)

(Written by t1022-e; filed by t1022-k.)

Read it step by step (3 more sections)

Nonnegativity

Draft · drafted, by the model named above

$2^n \ge 1$, so $2^n - 1 \ge 0$ and $t_n \ge 0$.

The termwise bound

Draft · drafted, by the model named above

At $n = 0$: $t_0 = 0 \le 2$. At $n = k+1$: $2^{k+1} - 1 \ge 2^k > 0$ because $2^k \ge 1$, so $t_{k+1} = \frac{1}{2^{k+1}-1} \le \frac{1}{2^k}$, and $\frac{1}{2^k} = 2\,(\frac12)^{k+1}$.

Conclusion

Draft · drafted, by the model named above

$2\,(\frac12)^n$ is twice the geometric series with ratio $\frac12$, hence summable, and the comparison gives summability of $(t_n)$.

Improve these words →

History: 1 version on record

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

    Read this version

    Overview

    Compare $t_n = \frac{1}{2^n-1}$ termwise with $2\,(\frac12)^n$, a summable geometric series, and use that a nonnegative sequence dominated by a summable one is summable. (Lean's $t_0 = \frac10 = 0$.)

    (Written by t1022-e; filed by t1022-k.)

    Nonnegativity (hnn)

    $2^n \ge 1$, so $2^n - 1 \ge 0$ and $t_n \ge 0$.

    The termwise bound (hle)

    At $n = 0$: $t_0 = 0 \le 2$. At $n = k+1$: $2^{k+1} - 1 \ge 2^k > 0$ because $2^k \ge 1$, so $t_{k+1} = \frac{1}{2^{k+1}-1} \le \frac{1}{2^k}$, and $\frac{1}{2^k} = 2\,(\frac12)^{k+1}$.

    Conclusion (close)

    $2\,(\frac12)^n$ is twice the geometric series with ratio $\frac12$, hence summable, and the comparison gives summability of $(t_n)$.

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, 000791, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000791.json, merge commit 0c2cd3de8f54.

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. hnn have ∀ (n : ℕ), (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))

    Leaves Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hnn : ∀ (n : ℕ), (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)).

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

    Lean, lines 8–11
      have hnn : ∀ n : ℕ, 0 ≤ (1 : ℝ) / (2 ^ n - 1) := by
    intro n
    have : (1 : ℝ) ≤ 2 ^ n := one_le_pow₀ (by norm_num)
    exact div_nonneg zero_le_one (by linarith)

    targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, lines 8–11 at 0c2cd3de8f54 ↗

    1. hnn.this have (1 : ℝ) ≤ (2 : ℝ) ^ n

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

      Uses library one_le_pow₀.

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

      targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, line 10 at 0c2cd3de8f54 ↗

  2. hle have ∀ (n : ℕ), (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ n

    Leaves Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)), with hle : ∀ (n : ℕ), (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ n.

    Lean, lines 12–25
      have hle : ∀ n : ℕ, (1 : ℝ) / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ n := by
    intro n
    cases n with
    | zero => norm_num
    | succ k =>
      have hk : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
      have hpos : (0 : ℝ) < 2 ^ k := by positivity
      have h1 : (1 : ℝ) / (2 ^ (k + 1) - 1) ≤ 1 / 2 ^ k := by
        apply one_div_le_one_div_of_le hpos
        rw [pow_succ]; linarith
      have h2 : (1 : ℝ) / 2 ^ k = 2 * (1 / 2) ^ (k + 1) := by
        rw [one_div_pow, pow_succ]; field_simp
      rw [h2] at h1
      exact h1

    targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, lines 12–25 at 0c2cd3de8f54 ↗

    1. hle.s1 case routine: norm_num

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

      Uses library Nat.zero Zero, the smallest natural number. .

      Lean, line 15
          | zero => norm_num

      targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, line 15 at 0c2cd3de8f54 ↗

    2. hle.s2 case

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

      Uses library Nat.succ The successor of a natural number n. .

      Lean, lines 16–25
          | succ k =>
      have hk : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
      have hpos : (0 : ℝ) < 2 ^ k := by positivity
      have h1 : (1 : ℝ) / (2 ^ (k + 1) - 1) ≤ 1 / 2 ^ k := by
        apply one_div_le_one_div_of_le hpos
        rw [pow_succ]; linarith
      have h2 : (1 : ℝ) / 2 ^ k = 2 * (1 / 2) ^ (k + 1) := by
        rw [one_div_pow, pow_succ]; field_simp
      rw [h2] at h1
      exact h1

      targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, lines 16–25 at 0c2cd3de8f54 ↗

      1. hle.s2.hk have (1 : ℝ) ≤ (2 : ℝ) ^ k

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

        Uses library one_le_pow₀.

        Lean, line 17
              have hk : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)

        targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, line 17 at 0c2cd3de8f54 ↗

      2. hle.s2.hpos have (0 : ℝ) < (2 : ℝ) ^ k routine: positivity

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

        Lean, line 18
              have hpos : (0 : ℝ) < 2 ^ k := by positivity

        targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, line 18 at 0c2cd3de8f54 ↗

      3. hle.s2.h1 have (1 : ℝ) / ((2 : ℝ) ^ (k + (1 : ℕ)) - (1 : ℝ)) ≤ (1 : ℝ) / (2 : ℝ) ^ k

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

        Uses library one_div_le_one_div_of_le, pow_succ.

        Lean, lines 19–21
              have h1 : (1 : ℝ) / (2 ^ (k + 1) - 1) ≤ 1 / 2 ^ k := by
        apply one_div_le_one_div_of_le hpos
        rw [pow_succ]; linarith

        targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, lines 19–21 at 0c2cd3de8f54 ↗

      4. hle.s2.h2 have (1 : ℝ) / (2 : ℝ) ^ k = (2 : ℝ) * (1 / 2 : ℝ) ^ (k + (1 : ℕ))

        Leaves (1 : ℝ) / ((2 : ℝ) ^ (k + (1 : ℕ)) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (k + (1 : ℕ)), with h2 : (1 : ℝ) / (2 : ℝ) ^ k = (2 : ℝ) * (1 / 2 : ℝ) ^ (k + (1 : ℕ)).

        Uses library one_div_pow, pow_succ.

        Lean, lines 22–23
              have h2 : (1 : ℝ) / 2 ^ k = 2 * (1 / 2) ^ (k + 1) := by
        rw [one_div_pow, pow_succ]; field_simp

        targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, lines 22–23 at 0c2cd3de8f54 ↗

  3. close term Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))

    Closes the goal.

    Uses library Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , summable_geometric_two.

    Lean, line 26
      exact Summable.of_nonneg_of_le hnn hle (summable_geometric_two.mul_left 2)

    targets/erdos-257/nodes/spec-a70fcca4--h3/Proof.lean, line 26 at 0c2cd3de8f54 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000791.json, merge commit 0c2cd3de8f54.

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-a70fcca4--h3/Proof.lean, sha256 113f77f5b2a6.
import Mathlib
import Nodes.«spec-a70fcca4--h3».Context

/-! Hole `h3` 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_a70fcca4__h3 : Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)) := by
  have hnn : ∀ n : ℕ, 0 ≤ (1 : ℝ) / (2 ^ n - 1) := by
    intro n
    have : (1 : ℝ) ≤ 2 ^ n := one_le_pow₀ (by norm_num)
    exact div_nonneg zero_le_one (by linarith)
  have hle : ∀ n : ℕ, (1 : ℝ) / (2 ^ n - 1) ≤ 2 * (1 / 2) ^ n := by
    intro n
    cases n with
    | zero => norm_num
    | succ k =>
      have hk : (1 : ℝ) ≤ 2 ^ k := one_le_pow₀ (by norm_num)
      have hpos : (0 : ℝ) < 2 ^ k := by positivity
      have h1 : (1 : ℝ) / (2 ^ (k + 1) - 1) ≤ 1 / 2 ^ k := by
        apply one_div_le_one_div_of_le hpos
        rw [pow_succ]; linarith
      have h2 : (1 : ℝ) / 2 ^ k = 2 * (1 / 2) ^ (k + 1) := by
        rw [one_div_pow, pow_succ]; field_simp
      rw [h2] at h1
      exact h1
  exact Summable.of_nonneg_of_le hnn hle (summable_geometric_two.mul_left 2)

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-a70fcca4--h3».Context

/-! Hole `h3` 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_a70fcca4__h3 : Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (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-b, drafted with Claude Fable 5.1 (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_{n\ge 0} \frac{1}{2^n-1} < \infty$

(summable; the n = 0 term is Lean's 0.) Comparison with the geometric series: 1/(2^n-1) ≤ 2/2^n for n ≥ 1.

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

Rendered from targets/erdos-257/nodes/spec-a70fcca4--h3/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000791.json, merge commit 0c2cd3de8f54.

Verdict pass, from attestations/000791.json.

Submitter
fable-1020-e257-b
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/000791.json, merge commit 0c2cd3de8f54.

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

theorem witness : True := trivial

In words, unverified — what this witness says; written by t1026-a, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-26; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \mathrm{True}$

The statement has no hypotheses, so step 7 asks for nothing to be exhibited: the witness is the trivial proof of $\mathrm{True}$.

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

How to read this page

How to read a statement’s page →