Summability of the prime sum 1/(2^p - 1)

spec-2e765953 Opn.erdos_69_summable_prime_reciprocal

proved

Proposed by a contributor.

$\displaystyle \sum_{p\ \text{prime}}\frac{1}{2^{p}-1} < \infty$

The family p ↦ 1/(2^p − 1), indexed by the primes and valued in ℝ, is summable in Mathlib's sense (unconditionally; for a nonnegative real family this is ordinary convergence).

unverified · history

Lean

theorem Opn.erdos_69_summable_prime_reciprocal :
    Summable (fun p : Nat.Primes => (1 : ℝ) / (2 ^ (p : ℕ) - 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 →

How it was proved

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000302.json, merge commit f606a87ee3a9.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 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.

hg have Summable fun (n : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ n
Leaves Summable fun (p : Nat.Primes) => (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hg : Summable fun (n : ℕ) => (2 : ℝ) * (1 / 2 : ℝ) ^ n.
Uses library Summable, summable_geometric_two.
Lean, lines 8–9
```
  have hg : Summable (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) :=
    summable_geometric_two.mul_left 2
```
targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 8–9 at f606a87ee3a9 ↗
hsub have Summable fun (p : Nat.Primes) => (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ)
Leaves Summable fun (p : Nat.Primes) => (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with hsub : Summable fun (p : Nat.Primes) => (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ).
Uses library Summable, Nat.Primes, Subtype.val_injective.
Lean, lines 10–11
```
  have hsub : Summable (fun p : Nat.Primes => (2 : ℝ) * (1 / 2) ^ (p : ℕ)) :=
    hg.comp_injective Subtype.val_injective
```
targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 10–11 at f606a87ee3a9 ↗
s3 case
Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)).
Lean, lines 13–15
```
  · have h1 : (1 : ℝ) ≤ 2 ^ (p : ℕ) := one_le_pow₀ (by norm_num)
    have h0 : (0 : ℝ) ≤ 2 ^ (p : ℕ) - 1 := by linarith
    positivity
```
targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 13–15 at f606a87ee3a9 ↗
1. s3.h1 have (1 : ℝ) ≤ (2 : ℝ) ^ (↑p : ℕ)
  Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with h1 : (1 : ℝ) ≤ (2 : ℝ) ^ (↑p : ℕ).
  Uses library one_le_pow₀.
  Lean, line 13
  · have h1 : (1 : ℝ) ≤ 2 ^ (p : ℕ) := one_le_pow₀ (by norm_num)
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, line 13 at f606a87ee3a9 ↗
2. s3.h0 have (0 : ℝ) ≤ (2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ) routine: linarith
  Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)), with h0 : (0 : ℝ) ≤ (2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ).
  Lean, line 14
  have h0 : (0 : ℝ) ≤ 2 ^ (p : ℕ) - 1 := by linarith
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, line 14 at f606a87ee3a9 ↗
s4 case
Leaves (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ).
Lean, lines 16–30
```
  · have hp : 1 ≤ (p : ℕ) := p.2.one_lt.le
    have h2 : (2 : ℝ) ^ (p : ℕ) = 2 * 2 ^ ((p : ℕ) - 1) := by
      rw [← pow_succ']
      congr 1
      omega
    have hpos : (0 : ℝ) < 2 ^ ((p : ℕ) - 1) := by positivity
    have hden : (2 : ℝ) ^ ((p : ℕ) - 1) ≤ 2 ^ (p : ℕ) - 1 := by
      have h1 : (1 : ℝ) ≤ 2 ^ ((p : ℕ) - 1) := one_le_pow₀ (by norm_num)
      rw [h2]
      linarith
    calc (1 : ℝ) / (2 ^ (p : ℕ) - 1) ≤ 1 / 2 ^ ((p : ℕ) - 1) :=
          one_div_le_one_div_of_le hpos hden
      _ = 2 * (1 / 2) ^ (p : ℕ) := by
          rw [one_div_pow, h2]
          field_simp
```
targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 16–30 at f606a87ee3a9 ↗
1. s4.hp have (1 : ℕ) ≤ (↑p : ℕ)
  Leaves (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ), with hp : (1 : ℕ) ≤ (↑p : ℕ).
  Lean, line 16
  · have hp : 1 ≤ (p : ℕ) := p.2.one_lt.le
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, line 16 at f606a87ee3a9 ↗
2. s4.h2 have (2 : ℝ) ^ (↑p : ℕ) = (2 : ℝ) * (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ))
  Leaves (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ), with h2 : (2 : ℝ) ^ (↑p : ℕ) = (2 : ℝ) * (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)).
  Uses library pow_succ'.
  Lean, lines 17–20
  have h2 : (2 : ℝ) ^ (p : ℕ) = 2 * 2 ^ ((p : ℕ) - 1) := by rw [← pow_succ'] congr 1 omega
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 17–20 at f606a87ee3a9 ↗
3. s4.hpos have (0 : ℝ) < (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)) routine: positivity
  Leaves (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ), with hpos : (0 : ℝ) < (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)).
  Lean, line 21
  have hpos : (0 : ℝ) < 2 ^ ((p : ℕ) - 1) := by positivity
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, line 21 at f606a87ee3a9 ↗
4. s4.hden have (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)) ≤ (2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)
  Leaves (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ (2 : ℝ) * (1 / 2 : ℝ) ^ (↑p : ℕ), with hden : (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)) ≤ (2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ).
  Lean, lines 22–25
  have hden : (2 : ℝ) ^ ((p : ℕ) - 1) ≤ 2 ^ (p : ℕ) - 1 := by have h1 : (1 : ℝ) ≤ 2 ^ ((p : ℕ) - 1) := one_le_pow₀ (by norm_num) rw [h2] linarith
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 22–25 at f606a87ee3a9 ↗
  s4.hden.h1 have (1 : ℝ) ≤ (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ))
  Leaves (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)) ≤ (2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ), with h1 : (1 : ℝ) ≤ (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ)).
  Uses library one_le_pow₀.
  Lean, line 23
  have h1 : (1 : ℝ) ≤ 2 ^ ((p : ℕ) - 1) := one_le_pow₀ (by norm_num)
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, line 23 at f606a87ee3a9 ↗
5. s4.s5 calc (1 : ℝ) / ((2 : ℝ) ^ (↑p : ℕ) - (1 : ℝ)) ≤ (1 : ℝ) / (2 : ℝ) ^ ((↑p : ℕ) - (1 : ℕ))
  Closes the goal.
  Uses library one_div_le_one_div_of_le.
  Lean, lines 26–27
  calc (1 : ℝ) / (2 ^ (p : ℕ) - 1) ≤ 1 / 2 ^ ((p : ℕ) - 1) := one_div_le_one_div_of_le hpos hden
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 26–27 at f606a87ee3a9 ↗
6. s4.s6 calc
  Closes the goal.
  Uses library one_div_pow.
  Lean, lines 28–30
  _ = 2 * (1 / 2) ^ (p : ℕ) := by rw [one_div_pow, h2] field_simp
  targets/erdos-69/nodes/spec-2e765953/Proof.lean, lines 28–30 at f606a87ee3a9 ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/spec-2e765953/Proof.lean, sha256 b34e84a4542b.

import Mathlib
import Nodes.«spec-2e765953».Context

/-- The prime-indexed Lambert series of the root's identity converges: the sum over primes `p`
of `1 / (2 ^ p - 1)` is summable in ℝ. This is the right-hand side of `erdos-69--h1-v2`. -/
theorem Opn.erdos_69_summable_prime_reciprocal :
    Summable (fun p : Nat.Primes => (1 : ℝ) / (2 ^ (p : ℕ) - 1)) := by
  have hg : Summable (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) :=
    summable_geometric_two.mul_left 2
  have hsub : Summable (fun p : Nat.Primes => (2 : ℝ) * (1 / 2) ^ (p : ℕ)) :=
    hg.comp_injective Subtype.val_injective
  refine Summable.of_nonneg_of_le (fun p => ?_) (fun p => ?_) hsub
  · have h1 : (1 : ℝ) ≤ 2 ^ (p : ℕ) := one_le_pow₀ (by norm_num)
    have h0 : (0 : ℝ) ≤ 2 ^ (p : ℕ) - 1 := by linarith
    positivity
  · have hp : 1 ≤ (p : ℕ) := p.2.one_lt.le
    have h2 : (2 : ℝ) ^ (p : ℕ) = 2 * 2 ^ ((p : ℕ) - 1) := by
      rw [← pow_succ']
      congr 1
      omega
    have hpos : (0 : ℝ) < 2 ^ ((p : ℕ) - 1) := by positivity
    have hden : (2 : ℝ) ^ ((p : ℕ) - 1) ≤ 2 ^ (p : ℕ) - 1 := by
      have h1 : (1 : ℝ) ≤ 2 ^ ((p : ℕ) - 1) := one_le_pow₀ (by norm_num)
      rw [h2]
      linarith
    calc (1 : ℝ) / (2 ^ (p : ℕ) - 1) ≤ 1 / 2 ^ ((p : ℕ) - 1) :=
          one_div_le_one_div_of_le hpos hden
      _ = 2 * (1 / 2) ^ (p : ℕ) := by
          rw [one_div_pow, h2]
          field_simp

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

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-2e765953».Context

/-- The prime-indexed Lambert series of the root's identity converges: the sum over primes `p`
of `1 / (2 ^ p - 1)` is summable in ℝ. This is the right-hand side of `erdos-69--h1-v2`. -/
theorem Opn.erdos_69_summable_prime_reciprocal :
    Summable (fun p : Nat.Primes => (1 : ℝ) / (2 ^ (p : ℕ) - 1)) := by
  sorry

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

Draft · drafted, by the model named above

$\displaystyle \sum_{p\ \text{prime}}\frac{1}{2^{p}-1} < \infty$

The family p ↦ 1/(2^p − 1), indexed by the primes and valued in ℝ, is summable in Mathlib's sense (unconditionally; for a nonnegative real family this is ordinary convergence).

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

Rendered from targets/erdos-69/nodes/spec-2e765953/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000302.json, merge commit f606a87ee3a9.

Verdict pass, from attestations/000302.json.

Submitter: t0929-4
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/spec-2e765953/Witness.lean, sha256 fba89731e33c.

import Mathlib

/-! Non-vacuity witness (D-4 step 7): the statement has no hypotheses, so the expected
witness type is `True`. -/

theorem witness : True := trivial

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 →

Acknowledged findings (1)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / (2 ^ ↑p - 1)

For a prime p, p >= 2, so the real divisor 2^p - 1 is at least 3 and never 0; no term takes Lean's junk value. The expression is the right-hand side of the proved erdos-69--h1-v2 as written there.

How to read this page

How to read a statement’s page →