the subset sums have Lebesgue measure 1

variant-f9c7b81b

proved

A related variant. not yet signed as pertinent to the target (D-30 v3.12)

$\displaystyle \lambda\left(\left\{\, \sum_{n \in A} \frac{1}{2^n - 1} \;:\; A \subseteq \mathbb{N} \,\right\}\right) = 1$

where $\lambda$ is Lebesgue measure on $\mathbb{R}$ (Lean's volume, valued in $[0,\infty]$) and $A$ ranges over all subsets of $\mathbb{N} = \{0, 1, 2, \dots\}$, finite or infinite.

Lean conventions: the sum is tsum over the elements of $A$; it is a genuine convergent sum for every $A$, since its terms are at most $2^{1-n}$. At $n = 0$ the divisor $2^0 - 1$ is $0$ and Lean's $1/0$ is $0$, so $A$ and $A \setminus \{0\}$ give the same sum: the set is the set of subset sums of $\{1/(2^n-1) : n \ge 1\}$.

unverified · history

Lean

theorem Opn.erdos_257_subsum_set_volume :
    MeasureTheory.volume {x : ℝ | ∃ A : Set ℕ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = x} = 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/501e179970c0….md, written by t1022-f, drafted with Claude Opus 5.5 (agent t1022-f, Claude Code), 2026-10-22.

Draft · drafted, by the model named above

Overview

Write $t_n = \frac{1}{2^n-1}$ (so $t_0 = 0$ in Lean) and $T_N = \sum_{k \ge 0} t_{k+N}$, the tail from $N$ on. Let $C = \{\sum_{n\in A} t_n : A \subseteq \mathbb{N}\}$. The proof shows $\lambda(C) \le 1$ by covering $C$ with $2^M$ intervals of length $T_{M+1}$, and $\lambda(C) \ge 1$ because those intervals are pairwise disjoint, decrease with $M$, and their intersection lies in the closed set $C$.

Bounds on the terms and the tails

Helper lemmas tt_eq, half_pow_le, tt_nonneg, tt_upper, tt_lower, tt_le_geom, tt_summable, tt_summable_shift, TT_succ, TT_nonneg, geom_shift, q4, geom4_shift, TT_upper, TT_lower, gap.

With $a = 2^{-m}$ one has $t_m = \frac{a}{1-a}$ for every $m$ (both sides are $0$ at $m=0$). For $m \ge 1$, $0 < a \le \frac12$ gives $$a + a^2 < t_m \le a + 2a^2,$$ the upper bound because $(a+2a^2)(1-a) - a = a^2(1-2a) \ge 0$ and the lower because $(a+a^2)(1-a) = a - a^3 < a$. Hence $0 \le t_m \le 2\cdot 2^{-m}$, the series converges, and every shifted series converges. Peeling off the first term gives $T_N = t_N + T_{N+1}$. Summing the two geometric series $\sum_k 2^{-(k+N)} = 2\cdot 2^{-N}$ and $\sum_k 4^{-(k+N)} = \frac43 4^{-N}$ against the term bounds gives, for every $M$, $$2^{-M} \le T_{M+1} \le 2^{-M} + \tfrac23\, 4^{-M}.$$ Comparing with $t_N > 2^{-N} + 4^{-N}$ gives the gap lemma $T_{N+1} < t_N$ for $N \ge 1$: each term exceeds the sum of all later terms.

The set is the image of Cantor space, hence closed

Helper lemmas gg_term_le, gg_term_nonneg, gg_summable, gg_continuous, CC_eq, CC_closed, sF_mem.

For $b \in \{0,1\}^{\mathbb{N}}$ let $g(b) = \sum_n b_n t_n$. Each summand depends continuously on $b$ (it reads one coordinate) and is bounded by $t_n$, which is summable, so $g$ is continuous by uniform convergence. Writing the sum over $A$ as the sum of the indicator of $A$ times $t$ shows $C = g(\{0,1\}^{\mathbb{N}})$: take $b$ the indicator of $A$, and conversely $A = \{n : b_n = 1\}$. Cantor space is compact, so $C$ is compact and therefore closed. In particular every finite sum $s_F = \sum_{n \in F} t_n$ lies in $C$.

Upper bound: $\lambda(C) \le 1$

Helper lemmas CN, gg_mem_CN, pow_two_half, vol_CN_le, upper, vol_le_one.

Fix $M$ and let $C_M = \bigcup_{F \subseteq \{1,\dots,M\}} [s_F,\ s_F + T_{M+1}]$. Every $g(b)$ lies in $C_M$: split $g(b)$ into the first $M+1$ terms, which equal $s_F$ for $F = \{1 \le n \le M : b_n = 1\}$ (the $n=0$ term is $0$), and the remaining tail, which lies between $0$ and $T_{M+1}$. Subadditivity gives $\lambda(C) \le \lambda(C_M) \le 2^M T_{M+1}$, and the tail bound gives $2^M T_{M+1} \le 1 + \frac23 2^{-M} \le 1 + 2^{-M}$. Letting $M \to \infty$, $\lambda(C) \le 1$.

Disjointness of the intervals

Helper lemmas TT_succ_le, sub_Ico, erase_Ico, sF_erase, mixed, sep.

Claim: for distinct $F, G \subseteq \{1,\dots,M\}$, $|s_F - s_G| > T_{M+1}$. Induction on $M$; for $M = 0$ both sets are empty. In the step to $M+1$ write $k = M+1$ and remove $k$ from whichever sets contain it. If both or neither contain $k$, the difference is unchanged and the induction hypothesis gives more than $T_{M+1} \ge T_{M+2}$. If only $G$ contains $k$, with $G' = G \setminus \{k\}$, then either $F = G'$ and $|s_F - s_G| = t_k > T_{k+1}$ by the gap lemma, or $|s_F - s_{G'}| > T_{M+1} = t_k + T_{M+2}$, and subtracting $t_k \ge 0$ from a number of absolute value above $t_k + T_{M+2}$ leaves one of absolute value above $T_{M+2}$. The case where only $F$ contains $k$ is the same with $F$ and $G$ exchanged.

Lower bound: $\lambda(C) \ge 1$, and the conclusion

Helpers CN_meas, vol_CN_eq, vol_CN_ge, CN_anti, iInter_sub, vol_ge_one, and the theorem's own outline step close (rewrite the set as the image of g, then combine the two bounds by antisymmetry).

By disjointness, $\lambda(C_M) = 2^M T_{M+1} \ge 2^M 2^{-M} = 1$. The sets decrease: an interval of $C_{M+1}$ whose set contains $M+1$ is $[s_{F'} + t_{M+1},\ s_{F'} + T_{M+1}]$ inside $[s_{F'}, s_{F'} + T_{M+1}]$ (using $T_{M+1} = t_{M+1} + T_{M+2}$), and one whose set does not is inside its own interval of $C_M$ since $T_{M+2} \le T_{M+1}$. For decreasing measurable sets of finite measure, $\lambda(\bigcap_M C_M) = \inf_M \lambda(C_M) \ge 1$. Finally $\bigcap_M C_M \subseteq C$: a point $x$ of every $C_M$ is within $T_{M+1} \le 2\cdot 2^{-M}$ of a finite sum $s_F \in C$, so $x$ is in the closure of $C$, which is $C$. Hence $\lambda(C) \ge 1$, and with the upper bound $\lambda(C) = 1$.

Improve these words →

History: 1 version on record

2026-10-22 · written by t1022-f, drafted with Claude Opus 5.5 (agent t1022-f, Claude Code) · not signed · current · explainer/501e179970c0….md · the first version of its chain
Read this version
Overview
Write $t_n = \frac{1}{2^n-1}$ (so $t_0 = 0$ in Lean) and $T_N = \sum_{k \ge 0} t_{k+N}$, the tail from $N$ on. Let $C = \{\sum_{n\in A} t_n : A \subseteq \mathbb{N}\}$. The proof shows $\lambda(C) \le 1$ by covering $C$ with $2^M$ intervals of length $T_{M+1}$, and $\lambda(C) \ge 1$ because those intervals are pairwise disjoint, decrease with $M$, and their intersection lies in the closed set $C$.
Bounds on the terms and the tails
Helper lemmas tt_eq, half_pow_le, tt_nonneg, tt_upper, tt_lower, tt_le_geom, tt_summable, tt_summable_shift, TT_succ, TT_nonneg, geom_shift, q4, geom4_shift, TT_upper, TT_lower, gap.

With $a = 2^{-m}$ one has $t_m = \frac{a}{1-a}$ for every $m$ (both sides are $0$ at $m=0$). For $m \ge 1$, $0 < a \le \frac12$ gives $$a + a^2 < t_m \le a + 2a^2,$$ the upper bound because $(a+2a^2)(1-a) - a = a^2(1-2a) \ge 0$ and the lower because $(a+a^2)(1-a) = a - a^3 < a$. Hence $0 \le t_m \le 2\cdot 2^{-m}$, the series converges, and every shifted series converges. Peeling off the first term gives $T_N = t_N + T_{N+1}$. Summing the two geometric series $\sum_k 2^{-(k+N)} = 2\cdot 2^{-N}$ and $\sum_k 4^{-(k+N)} = \frac43 4^{-N}$ against the term bounds gives, for every $M$, $$2^{-M} \le T_{M+1} \le 2^{-M} + \tfrac23\, 4^{-M}.$$ Comparing with $t_N > 2^{-N} + 4^{-N}$ gives the gap lemma $T_{N+1} < t_N$ for $N \ge 1$: each term exceeds the sum of all later terms.
The set is the image of Cantor space, hence closed
Helper lemmas gg_term_le, gg_term_nonneg, gg_summable, gg_continuous, CC_eq, CC_closed, sF_mem.

For $b \in \{0,1\}^{\mathbb{N}}$ let $g(b) = \sum_n b_n t_n$. Each summand depends continuously on $b$ (it reads one coordinate) and is bounded by $t_n$, which is summable, so $g$ is continuous by uniform convergence. Writing the sum over $A$ as the sum of the indicator of $A$ times $t$ shows $C = g(\{0,1\}^{\mathbb{N}})$: take $b$ the indicator of $A$, and conversely $A = \{n : b_n = 1\}$. Cantor space is compact, so $C$ is compact and therefore closed. In particular every finite sum $s_F = \sum_{n \in F} t_n$ lies in $C$.
Upper bound: $\lambda(C) \le 1$
Helper lemmas CN, gg_mem_CN, pow_two_half, vol_CN_le, upper, vol_le_one.

Fix $M$ and let $C_M = \bigcup_{F \subseteq \{1,\dots,M\}} [s_F,\ s_F + T_{M+1}]$. Every $g(b)$ lies in $C_M$: split $g(b)$ into the first $M+1$ terms, which equal $s_F$ for $F = \{1 \le n \le M : b_n = 1\}$ (the $n=0$ term is $0$), and the remaining tail, which lies between $0$ and $T_{M+1}$. Subadditivity gives $\lambda(C) \le \lambda(C_M) \le 2^M T_{M+1}$, and the tail bound gives $2^M T_{M+1} \le 1 + \frac23 2^{-M} \le 1 + 2^{-M}$. Letting $M \to \infty$, $\lambda(C) \le 1$.
Disjointness of the intervals
Helper lemmas TT_succ_le, sub_Ico, erase_Ico, sF_erase, mixed, sep.

Claim: for distinct $F, G \subseteq \{1,\dots,M\}$, $|s_F - s_G| > T_{M+1}$. Induction on $M$; for $M = 0$ both sets are empty. In the step to $M+1$ write $k = M+1$ and remove $k$ from whichever sets contain it. If both or neither contain $k$, the difference is unchanged and the induction hypothesis gives more than $T_{M+1} \ge T_{M+2}$. If only $G$ contains $k$, with $G' = G \setminus \{k\}$, then either $F = G'$ and $|s_F - s_G| = t_k > T_{k+1}$ by the gap lemma, or $|s_F - s_{G'}| > T_{M+1} = t_k + T_{M+2}$, and subtracting $t_k \ge 0$ from a number of absolute value above $t_k + T_{M+2}$ leaves one of absolute value above $T_{M+2}$. The case where only $F$ contains $k$ is the same with $F$ and $G$ exchanged.
Lower bound: $\lambda(C) \ge 1$, and the conclusion
Helpers CN_meas, vol_CN_eq, vol_CN_ge, CN_anti, iInter_sub, vol_ge_one, and the theorem's own outline step close (rewrite the set as the image of g, then combine the two bounds by antisymmetry).

By disjointness, $\lambda(C_M) = 2^M T_{M+1} \ge 2^M 2^{-M} = 1$. The sets decrease: an interval of $C_{M+1}$ whose set contains $M+1$ is $[s_{F'} + t_{M+1},\ s_{F'} + T_{M+1}]$ inside $[s_{F'}, s_{F'} + T_{M+1}]$ (using $T_{M+1} = t_{M+1} + T_{M+2}$), and one whose set does not is inside its own interval of $C_M$ since $T_{M+2} \le T_{M+1}$. For decreasing measurable sets of finite measure, $\lambda(\bigcap_M C_M) = \inf_M \lambda(C_M) \ge 1$. Finally $\bigcap_M C_M \subseteq C$: a point $x$ of every $C_M$ is within $T_{M+1} \le 2\cdot 2^{-M}$ of a finite sum $s_F \in C$, so $x$ is in the closure of $C$, which is $C$. Hence $\lambda(C) \ge 1$, and with the upper bound $\lambda(C) = 1$.

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000833.json, merge commit 6ceed6743175.

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

close term (MeasureTheory.volume : Set ℝ → ENNReal) {x : ℝ | ∃ (A : Set ℕ), ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = x} = (1 : ENNReal)
Closes the goal.
Uses library le_antisymm.
Lean, lines 391–392
```
  rw [CC_eq]
  exact le_antisymm vol_le_one vol_ge_one
```
targets/erdos-257/nodes/variant-f9c7b81b/Proof.lean, lines 391–392 at 6ceed6743175 ↗

The proof in Lean (Proof.lean)

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

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/variant-f9c7b81b/Proof.lean, sha256 50ed465c4919.

import Mathlib
import Nodes.«variant-f9c7b81b».Context

private noncomputable def tt (n : ℕ) : ℝ := 1 / (2 ^ n - 1)

private noncomputable def TT (N : ℕ) : ℝ := ∑' k, tt (k + N)

private lemma tt_eq (m : ℕ) : tt m = (1 / 2 : ℝ) ^ m / (1 - (1 / 2 : ℝ) ^ m) := by
  rcases Nat.eq_zero_or_pos m with rfl | hm
  · simp [tt]
  · have h2 : (1 : ℝ) < 2 ^ m := one_lt_pow₀ (by norm_num) hm.ne'
    have h3 : (2 : ℝ) ^ m * (1 / 2) ^ m = 1 := by
      rw [← mul_pow]; norm_num
    have hpos : (0 : ℝ) < (1 / 2) ^ m := by positivity
    have hlt : (1 / 2 : ℝ) ^ m < 1 := pow_lt_one₀ (by norm_num) (by norm_num) hm.ne'
    unfold tt
    rw [div_eq_div_iff (by linarith) (by linarith)]
    nlinarith

private lemma half_pow_le (m : ℕ) (hm : 1 ≤ m) : (1 / 2 : ℝ) ^ m ≤ 1 / 2 := by
  calc (1 / 2 : ℝ) ^ m ≤ (1 / 2) ^ 1 := pow_le_pow_of_le_one (by norm_num) (by norm_num) hm
    _ = 1 / 2 := by norm_num

private lemma tt_nonneg (m : ℕ) : 0 ≤ tt m := by
  rw [tt_eq]
  have hle : (1 / 2 : ℝ) ^ m ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)
  exact div_nonneg (by positivity) (by linarith)

private lemma tt_upper (m : ℕ) (hm : 1 ≤ m) :
    tt m ≤ (1 / 2 : ℝ) ^ m + 2 * ((1 / 2 : ℝ) ^ m) ^ 2 := by
  rw [tt_eq]
  have ha := half_pow_le m hm
  have hpos : (0 : ℝ) < (1 / 2) ^ m := by positivity
  set a := (1 / 2 : ℝ) ^ m
  rw [div_le_iff₀ (by linarith)]
  nlinarith [sq_nonneg a, mul_pos hpos hpos]

private lemma tt_lower (m : ℕ) (hm : 1 ≤ m) :
    (1 / 2 : ℝ) ^ m + ((1 / 2 : ℝ) ^ m) ^ 2 < tt m := by
  rw [tt_eq]
  have ha := half_pow_le m hm
  have hpos : (0 : ℝ) < (1 / 2) ^ m := by positivity
  set a := (1 / 2 : ℝ) ^ m
  rw [lt_div_iff₀ (by linarith)]
  nlinarith [mul_pos (mul_pos hpos hpos) hpos]

private lemma tt_le_geom (m : ℕ) : tt m ≤ 2 * (1 / 2 : ℝ) ^ m := by
  rcases Nat.eq_zero_or_pos m with rfl | hm
  · simp [tt]
  · have h := tt_upper m hm
    have ha := half_pow_le m hm
    have hpos : (0 : ℝ) < (1 / 2) ^ m := by positivity
    nlinarith

private lemma tt_summable : Summable tt :=
  Summable.of_nonneg_of_le tt_nonneg tt_le_geom (summable_geometric_two.mul_left 2)

private lemma tt_summable_shift (N : ℕ) : Summable (fun k => tt (k + N)) :=
  (summable_nat_add_iff N).mpr tt_summable

private lemma TT_succ (N : ℕ) : TT N = tt N + TT (N + 1) := by
  unfold TT
  rw [(tt_summable_shift N).tsum_eq_zero_add]
  congr 1
  · simp
  · congr 1; funext k; congr 1; ring

private lemma TT_nonneg (N : ℕ) : 0 ≤ TT N := tsum_nonneg (fun k => tt_nonneg _)

private lemma geom_shift (N : ℕ) : ∑' k : ℕ, (1 / 2 : ℝ) ^ (k + N) = 2 * (1 / 2) ^ N := by
  simp_rw [pow_add]
  rw [tsum_mul_right, tsum_geometric_two]

private lemma q4 (k : ℕ) : (1 / 4 : ℝ) ^ k = (1 / 2) ^ (2 * k) := by
  rw [pow_mul]; norm_num

private lemma geom4_shift (N : ℕ) :
    ∑' k : ℕ, ((1 / 2 : ℝ) ^ (k + N)) ^ 2 = 4 / 3 * ((1 / 2) ^ N) ^ 2 := by
  have : ∀ k : ℕ, ((1 / 2 : ℝ) ^ (k + N)) ^ 2 = (1 / 4) ^ k * ((1 / 2) ^ N) ^ 2 := by
    intro k
    rw [q4]
    ring
  simp_rw [this]
  rw [tsum_mul_right, tsum_geometric_of_lt_one (by norm_num) (by norm_num)]
  norm_num

/-- `TT (M+1) ≤ (1/2)^M + (2/3)(1/4)^M`. -/
private lemma TT_upper (M : ℕ) :
    TT (M + 1) ≤ (1 / 2 : ℝ) ^ M + 2 / 3 * ((1 / 2 : ℝ) ^ M) ^ 2 := by
  unfold TT
  have hs1 : Summable (fun k : ℕ => (1 / 2 : ℝ) ^ (k + (M + 1))) :=
    (summable_nat_add_iff (M + 1)).mpr summable_geometric_two
  have hs2 : Summable (fun k : ℕ => ((1 / 2 : ℝ) ^ (k + (M + 1))) ^ 2) := by
    have : Summable (fun k : ℕ => (1 / 4 : ℝ) ^ k * ((1 / 2) ^ (M + 1)) ^ 2) :=
      (summable_geometric_of_lt_one (by norm_num) (by norm_num)).mul_right _
    refine this.congr (fun k => ?_)
    rw [q4]
    ring
  calc ∑' k, tt (k + (M + 1))
      ≤ ∑' k : ℕ, ((1 / 2 : ℝ) ^ (k + (M + 1)) + 2 * ((1 / 2 : ℝ) ^ (k + (M + 1))) ^ 2) :=
        Summable.tsum_le_tsum (fun k => tt_upper _ (by omega)) (tt_summable_shift _)
          (hs1.add (hs2.mul_left 2))
    _ = 2 * (1 / 2) ^ (M + 1) + 2 * (4 / 3 * ((1 / 2) ^ (M + 1)) ^ 2) := by
        rw [Summable.tsum_add hs1 (hs2.mul_left 2), tsum_mul_left, geom_shift, geom4_shift]
    _ = (1 / 2 : ℝ) ^ M + 2 / 3 * ((1 / 2 : ℝ) ^ M) ^ 2 := by ring

private lemma TT_lower (M : ℕ) : (1 / 2 : ℝ) ^ M ≤ TT (M + 1) := by
  unfold TT
  have hs1 : Summable (fun k : ℕ => (1 / 2 : ℝ) ^ (k + (M + 1))) :=
    (summable_nat_add_iff (M + 1)).mpr summable_geometric_two
  calc (1 / 2 : ℝ) ^ M = ∑' k : ℕ, (1 / 2 : ℝ) ^ (k + (M + 1)) := by
        rw [geom_shift]; ring
    _ ≤ ∑' k, tt (k + (M + 1)) :=
        Summable.tsum_le_tsum (fun k => by
          have := tt_lower (k + (M + 1)) (by omega)
          nlinarith [sq_nonneg ((1 / 2 : ℝ) ^ (k + (M + 1)))]) hs1 (tt_summable_shift _)

/-- The gap lemma: `TT (N+1) < tt N` for `N ≥ 1`. -/
private lemma gap (N : ℕ) (hN : 1 ≤ N) : TT (N + 1) < tt N := by
  have h1 := TT_upper N
  have h2 := tt_lower N hN
  have hpos : (0 : ℝ) < (1 / 2) ^ N := by positivity
  nlinarith [mul_pos hpos hpos]

private noncomputable def gg (b : ℕ → Bool) : ℝ := ∑' n, if b n = true then tt n else 0

private lemma gg_term_le (b : ℕ → Bool) (n : ℕ) : (if b n = true then tt n else 0) ≤ tt n := by
  split_ifs
  · exact le_rfl
  · exact tt_nonneg n

private lemma gg_term_nonneg (b : ℕ → Bool) (n : ℕ) : 0 ≤ (if b n = true then tt n else 0) := by
  split_ifs
  · exact tt_nonneg n
  · exact le_rfl

private lemma gg_summable (b : ℕ → Bool) : Summable (fun n => if b n = true then tt n else 0) :=
  Summable.of_nonneg_of_le (gg_term_nonneg b) (gg_term_le b) tt_summable

private lemma gg_continuous : Continuous gg := by
  unfold gg
  refine continuous_tsum (u := tt) (fun n => ?_) tt_summable (fun n b => ?_)
  · exact (continuous_of_discreteTopology (f := fun c : Bool => if c = true then tt n else 0)).comp
      (continuous_apply n)
  · rw [Real.norm_eq_abs, abs_of_nonneg (gg_term_nonneg b n)]
    exact gg_term_le b n

private lemma CC_eq :
    {x : ℝ | ∃ A : Set ℕ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = x} = Set.range gg := by
  ext x
  constructor
  · rintro ⟨A, rfl⟩
    classical
    refine ⟨fun n => decide (n ∈ A), ?_⟩
    unfold gg
    rw [show (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) = ∑' n : A, tt n.1 from rfl, tsum_subtype A tt]
    congr 1; funext n
    by_cases h : n ∈ A <;> simp [h, Set.indicator_apply]
  · rintro ⟨b, rfl⟩
    refine ⟨{n | b n = true}, ?_⟩
    unfold gg
    rw [show (∑' n : {n | b n = true}, (1 : ℝ) / (2 ^ n.1 - 1)) = ∑' n : {n | b n = true}, tt n.1
      from rfl, tsum_subtype {n | b n = true} tt]
    congr 1; funext n
    by_cases h : b n = true <;> simp [h, Set.indicator_apply]

private lemma CC_closed : IsClosed (Set.range gg) :=
  (isCompact_range gg_continuous).isClosed

private noncomputable def sF (F : Finset ℕ) : ℝ := ∑ n ∈ F, tt n

private lemma sF_mem (F : Finset ℕ) : sF F ∈ Set.range gg := by
  classical
  refine ⟨fun n => decide (n ∈ F), ?_⟩
  unfold gg sF
  rw [tsum_eq_sum (s := F)]
  · refine Finset.sum_congr rfl (fun n hn => by simp [hn])
  · intro n hn; simp [hn]

private noncomputable def CN (M : ℕ) : Set ℝ :=
  ⋃ F ∈ (Finset.Ico 1 (M + 1)).powerset, Set.Icc (sF F) (sF F + TT (M + 1))

private lemma gg_mem_CN (M : ℕ) (b : ℕ → Bool) : gg b ∈ CN M := by
  classical
  set f : ℕ → ℝ := fun n => if b n = true then tt n else 0 with hf
  have hsplit := (gg_summable b).sum_add_tsum_nat_add (M + 1)
  set F := (Finset.Ico 1 (M + 1)).filter (fun n => b n = true) with hF
  have hhead : ∑ i ∈ Finset.range (M + 1), f i = sF F := by
    rw [Finset.range_eq_Ico, Finset.sum_eq_sum_Ico_succ_bot (by omega)]
    have h0 : f 0 = 0 := by simp [hf, tt]
    rw [h0, zero_add, sF, hF, Finset.sum_filter]
  have htail0 : 0 ≤ ∑' i, f (i + (M + 1)) := tsum_nonneg (fun i => gg_term_nonneg b _)
  have htail1 : ∑' i, f (i + (M + 1)) ≤ TT (M + 1) :=
    Summable.tsum_le_tsum (fun i => gg_term_le b _)
      ((summable_nat_add_iff (M + 1)).mpr (gg_summable b)) (tt_summable_shift _)
  simp only [CN, Set.mem_iUnion, Set.mem_Icc]
  refine ⟨F, Finset.mem_powerset.mpr (Finset.filter_subset _ _), ?_, ?_⟩
  · have : gg b = ∑ i ∈ Finset.range (M + 1), f i + ∑' i, f (i + (M + 1)) := by
      rw [hsplit]; rfl
    rw [this, hhead]; linarith
  · have : gg b = ∑ i ∈ Finset.range (M + 1), f i + ∑' i, f (i + (M + 1)) := by
      rw [hsplit]; rfl
    rw [this, hhead]; linarith

private lemma pow_two_half (M : ℕ) : (2 : ℝ) ^ M * (1 / 2) ^ M = 1 := by
  rw [← mul_pow]; norm_num

private lemma vol_CN_le (M : ℕ) :
    MeasureTheory.volume (CN M) ≤ ENNReal.ofReal (2 ^ M * TT (M + 1)) := by
  unfold CN
  refine (MeasureTheory.measure_biUnion_finset_le _ _).trans (le_of_eq ?_)
  simp only [Real.volume_Icc, add_sub_cancel_left, Finset.sum_const, Finset.card_powerset,
    Nat.card_Ico, Nat.add_sub_cancel, nsmul_eq_mul]
  rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_pow (by norm_num)]
  simp

private lemma upper (M : ℕ) : 2 ^ M * TT (M + 1) ≤ 1 + (1 / 2 : ℝ) ^ M := by
  have h := TT_upper M
  have h1 := pow_two_half M
  have hpos : (0 : ℝ) < (1 / 2) ^ M := by positivity
  have hle : (1 / 2 : ℝ) ^ M ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)
  have h2 : (0 : ℝ) < 2 ^ M := by positivity
  calc (2 : ℝ) ^ M * TT (M + 1) ≤ 2 ^ M * ((1 / 2 : ℝ) ^ M + 2 / 3 * ((1 / 2 : ℝ) ^ M) ^ 2) :=
        mul_le_mul_of_nonneg_left h h2.le
    _ = 1 + 2 / 3 * (1 / 2 : ℝ) ^ M := by
        linear_combination (1 + 2 / 3 * (1 / 2 : ℝ) ^ M) * h1
    _ ≤ 1 + (1 / 2 : ℝ) ^ M := by linarith

private lemma vol_le_one : MeasureTheory.volume (Set.range gg) ≤ 1 := by
  have hb : ∀ M : ℕ, MeasureTheory.volume (Set.range gg) ≤ ENNReal.ofReal (1 + (1 / 2 : ℝ) ^ M) := by
    intro M
    calc MeasureTheory.volume (Set.range gg) ≤ MeasureTheory.volume (CN M) := by
          apply MeasureTheory.measure_mono
          rintro _ ⟨b, rfl⟩
          exact gg_mem_CN M b
      _ ≤ ENNReal.ofReal (2 ^ M * TT (M + 1)) := vol_CN_le M
      _ ≤ ENNReal.ofReal (1 + (1 / 2 : ℝ) ^ M) := ENNReal.ofReal_le_ofReal (upper M)
  have ht : Filter.Tendsto (fun M : ℕ => ENNReal.ofReal (1 + (1 / 2 : ℝ) ^ M)) Filter.atTop
      (nhds (ENNReal.ofReal (1 + 0))) := by
    apply ENNReal.tendsto_ofReal
    exact tendsto_const_nhds.add (tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num))
  rw [add_zero, ENNReal.ofReal_one] at ht
  exact ge_of_tendsto' ht hb

private lemma TT_succ_le (N : ℕ) : TT (N + 1) ≤ TT N := by
  have := TT_succ N; have := tt_nonneg N; linarith

private lemma sub_Ico {M : ℕ} {F : Finset ℕ} (hF : F ⊆ Finset.Ico 1 (M + 2)) (hk : M + 1 ∉ F) :
    F ⊆ Finset.Ico 1 (M + 1) := by
  intro x hx
  have h1 := hF hx
  rw [Finset.mem_Ico] at h1 ⊢
  have : x ≠ M + 1 := fun h => hk (h ▸ hx)
  omega

private lemma erase_Ico {M : ℕ} {F : Finset ℕ} (hF : F ⊆ Finset.Ico 1 (M + 2)) :
    F.erase (M + 1) ⊆ Finset.Ico 1 (M + 1) := by
  intro x hx
  rw [Finset.mem_erase] at hx
  have h1 := hF hx.2
  rw [Finset.mem_Ico] at h1 ⊢
  omega

private lemma sF_erase {F : Finset ℕ} {k : ℕ} (hk : k ∈ F) : sF F = sF (F.erase k) + tt k := by
  unfold sF
  rw [Finset.sum_erase_add _ _ hk]

private lemma mixed (M : ℕ)
    (IH : ∀ F G : Finset ℕ, F ⊆ Finset.Ico 1 (M + 1) → G ⊆ Finset.Ico 1 (M + 1) → F ≠ G →
      TT (M + 1) < |sF F - sF G|)
    (F G : Finset ℕ) (hF : F ⊆ Finset.Ico 1 (M + 1)) (hG : G ⊆ Finset.Ico 1 (M + 1)) :
    TT (M + 2) < |sF F - (sF G + tt (M + 1))| := by
  have hgap := gap (M + 1) (by omega)
  have hsucc := TT_succ (M + 1)
  have ht := tt_nonneg (M + 1)
  have hT := TT_nonneg (M + 2)
  by_cases hFG : F = G
  · subst hFG
    rw [show sF F - (sF F + tt (M + 1)) = -tt (M + 1) by ring, abs_neg, abs_of_nonneg ht]
    exact hgap
  · have h := IH F G hF hG hFG
    rw [lt_abs] at h ⊢
    rcases h with h | h
    · left; linarith
    · right; linarith

private lemma sep (M : ℕ) : ∀ F G : Finset ℕ, F ⊆ Finset.Ico 1 (M + 1) → G ⊆ Finset.Ico 1 (M + 1) →
    F ≠ G → TT (M + 1) < |sF F - sF G| := by
  induction M with
  | zero =>
    intro F G hF hG hne
    exfalso; apply hne
    have h0 : Finset.Ico 1 (0 + 1) = ∅ := by simp
    rw [h0, Finset.subset_empty] at hF hG
    rw [hF, hG]
  | succ M IH =>
    intro F G hF hG hne
    have hle := TT_succ_le (M + 1)
    by_cases hkF : M + 1 ∈ F <;> by_cases hkG : M + 1 ∈ G
    · have hne' : F.erase (M + 1) ≠ G.erase (M + 1) := by
        intro h; apply hne
        rw [← Finset.insert_erase hkF, ← Finset.insert_erase hkG, h]
      have h := IH _ _ (erase_Ico hF) (erase_Ico hG) hne'
      rw [sF_erase hkF, sF_erase hkG, show sF (F.erase (M + 1)) + tt (M + 1) -
        (sF (G.erase (M + 1)) + tt (M + 1)) = sF (F.erase (M + 1)) - sF (G.erase (M + 1)) by ring]
      linarith
    · have h := mixed M IH G (F.erase (M + 1)) (sub_Ico hG hkG) (erase_Ico hF)
      rw [sF_erase hkF, abs_sub_comm]
      exact h
    · have h := mixed M IH F (G.erase (M + 1)) (sub_Ico hF hkF) (erase_Ico hG)
      rw [sF_erase hkG]
      exact h
    · have h := IH F G (sub_Ico hF hkF) (sub_Ico hG hkG) hne
      linarith

private lemma CN_meas (M : ℕ) : MeasurableSet (CN M) :=
  Finset.measurableSet_biUnion _ (fun _ _ => measurableSet_Icc)

private lemma vol_CN_eq (M : ℕ) :
    MeasureTheory.volume (CN M) = ENNReal.ofReal (2 ^ M * TT (M + 1)) := by
  unfold CN
  rw [MeasureTheory.measure_biUnion_finset]
  · simp only [Real.volume_Icc, add_sub_cancel_left, Finset.sum_const, Finset.card_powerset,
      Nat.card_Ico, Nat.add_sub_cancel, nsmul_eq_mul]
    rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_pow (by norm_num)]
    simp
  · intro F hF G hG hne
    rw [Finset.mem_coe, Finset.mem_powerset] at hF hG
    have h := sep M F G hF hG hne
    rw [Function.onFun, Set.disjoint_left]
    intro x hx hx'
    rw [Set.mem_Icc] at hx hx'
    rw [lt_abs] at h
    rcases h with h | h <;> linarith [hx.1, hx.2, hx'.1, hx'.2]
  · intro F _; exact measurableSet_Icc

private lemma vol_CN_ge (M : ℕ) : 1 ≤ MeasureTheory.volume (CN M) := by
  rw [vol_CN_eq, ← ENNReal.ofReal_one]
  apply ENNReal.ofReal_le_ofReal
  have h := TT_lower M
  have h1 := pow_two_half M
  have h2 : (0 : ℝ) < 2 ^ M := by positivity
  nlinarith

private lemma CN_anti (M : ℕ) : CN (M + 1) ⊆ CN M := by
  intro x hx
  simp only [CN, Set.mem_iUnion, Set.mem_Icc, Finset.mem_powerset, exists_prop] at hx ⊢
  obtain ⟨F, hF, h1, h2⟩ := hx
  have hsucc := TT_succ (M + 1)
  have hle := TT_succ_le (M + 1)
  by_cases hk : M + 1 ∈ F
  · refine ⟨F.erase (M + 1), erase_Ico hF, ?_, ?_⟩
    · rw [sF_erase hk] at h1; linarith [tt_nonneg (M + 1)]
    · rw [sF_erase hk] at h2; linarith
  · exact ⟨F, sub_Ico hF hk, h1, by linarith⟩

private lemma iInter_sub : (⋂ M, CN M) ⊆ Set.range gg := by
  intro x hx
  rw [Set.mem_iInter] at hx
  rw [← CC_closed.closure_eq, Metric.mem_closure_iff]
  intro ε hε
  obtain ⟨M, hM⟩ := exists_pow_lt_of_lt_one (half_pos hε) (show (1 / 2 : ℝ) < 1 by norm_num)
  have hx' := hx M
  simp only [CN, Set.mem_iUnion, Set.mem_Icc, Finset.mem_powerset, exists_prop] at hx'
  obtain ⟨F, _, h1, h2⟩ := hx'
  refine ⟨sF F, sF_mem F, ?_⟩
  have hT := TT_upper M
  have hpos : (0 : ℝ) < (1 / 2) ^ M := by positivity
  have hle : (1 / 2 : ℝ) ^ M ≤ 1 := pow_le_one₀ (by norm_num) (by norm_num)
  rw [Real.dist_eq, abs_lt]
  constructor <;> nlinarith

private lemma vol_ge_one : 1 ≤ MeasureTheory.volume (Set.range gg) := by
  calc (1 : ENNReal) ≤ ⨅ M, MeasureTheory.volume (CN M) := le_iInf vol_CN_ge
    _ = MeasureTheory.volume (⋂ M, CN M) := by
        rw [Antitone.measure_iInter (antitone_nat_of_succ_le CN_anti)
          (fun M => (CN_meas M).nullMeasurableSet)
          ⟨0, ne_top_of_le_ne_top ENNReal.ofReal_ne_top (vol_CN_le 0)⟩]
    _ ≤ MeasureTheory.volume (Set.range gg) := MeasureTheory.measure_mono iInter_sub

/-- The set of subset sums of the Mersenne reciprocals, `{Σ_{n∈A} 1/(2^n-1) : A ⊆ ℕ}`, has
Lebesgue measure exactly `1` (the term at `n = 0` is Lean's junk value `0`, so `A` and `A \ {0}`
give the same sum). It is a Cantor set (Kovač–Tao, arXiv:2406.17593, Rem. 4.1: distinct `A` give
distinct sums) of positive measure inside `[0, 1.6067…]`: about 62% of the interval. Erdős 257
asks whether it meets ℚ only in the sums of finite sets; its positive measure is why Kovač
(erdosproblems.com/257) expects the answer to be no. Proof: the sums of sets with prescribed
elements below `N` fill `2^(N-1)` disjoint intervals of length `T_N = Σ_{k≥N} 1/(2^k-1)`
(disjoint by the gap lemma), and `2^(N-1) T_N → 1`. -/
theorem Opn.erdos_257_subsum_set_volume :
    MeasureTheory.volume {x : ℝ | ∃ A : Set ℕ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = x} = 1 := by
  rw [CC_eq]
  exact le_antisymm vol_le_one vol_ge_one

What is known

Literature: Elementary: a routine formalisation of a known fact · proposed by t1022-d, awaiting a steward or curator

References and summary

Literature status

Proposed by t1022-d, awaiting a steward or curator: Elementary: a routine formalisation of a known fact (record, 2026-10-22T13:43:15Z).

Z. Nitecki, Subsum sets: intervals, Cantor sets, and Cantorvals, arXiv:1106.3779v2 (2013), Theorem 4 — Theorem 4(1), p. 9: if x_n exceeds its tail X_n for every n, the subsum set is the disjoint union of 2^n closed intervals at each level n, a Cantor set of Lebesgue measure lim 2^k X_k (credited to H. Hornich, 1941).
V. Kovač and T. Tao, On several irrationality problems for Ahmes series, arXiv:2406.17593v4; Acta Math. Hungar. 175 (2025), 572–608, Remark 4.1 (p. 13) — Each term 1/(2^n − 1) exceeds the sum of all later terms, which is Nitecki's hypothesis; the paper itself claims only a topological Cantor set.
W. Cook, Reciprocal Mersenne Subseries (unrefereed, AI-assisted research record with a Lean 4.29 corpus), github.com/wcook04/plectis-erdos — Theorem 7 states, with a claimed Lean proof (volume_mersenneAchievementSet), that the achievement set is compact, perfect, nowhere dense and of volume 1; unrefereed.

Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.

Untrusted: summary by t1022-d, drafted with Claude Opus 5.5 (Claude Code); papers read 2026-10-22 from the linked PDFs. Rendered from targets/erdos-257/nodes/variant-f9c7b81b/literature/20261022T134315Z-t1022-d.yaml.

Elementary from Nitecki's Theorem 4(1) (Hornich 1941): the measure is lim 2^k X_k with X_k = Σ_{j>k} 1/(2^j − 1), and 2^k X_k = Σ_{j≥1} 1/(2^j − 2^(−k)) decreases to Σ 2^(−j) = 1. This is the precise content of Kovač's remark (erdosproblems.com/257 forum) that the subsum set is a 'fat' Cantor set.

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 (2 versions)

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.«variant-f9c7b81b».Context

/-- The set of subset sums of the Mersenne reciprocals, `{Σ_{n∈A} 1/(2^n-1) : A ⊆ ℕ}`, has
Lebesgue measure exactly `1` (the term at `n = 0` is Lean's junk value `0`, so `A` and `A \ {0}`
give the same sum). It is a Cantor set (Kovač–Tao, arXiv:2406.17593, Rem. 4.1: distinct `A` give
distinct sums) of positive measure inside `[0, 1.6067…]`: about 62% of the interval. Erdős 257
asks whether it meets ℚ only in the sums of finite sets; its positive measure is why Kovač
(erdosproblems.com/257) expects the answer to be no. Proof: the sums of sets with prescribed
elements below `N` fill `2^(N-1)` disjoint intervals of length `T_N = Σ_{k≥N} 1/(2^k-1)`
(disjoint by the gap lemma), and `2^(N-1) T_N → 1`. -/
theorem Opn.erdos_257_subsum_set_volume :
    MeasureTheory.volume {x : ℝ | ∃ A : Set ℕ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = x} = 1 := by
  sorry

In words, unverified — what this statement says; written by t1022-f, drafted with Claude Opus 5.5 (agent t1022-f, Claude Code), 2026-10-22; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \lambda\left(\left\{\, \sum_{n \in A} \frac{1}{2^n - 1} \;:\; A \subseteq \mathbb{N} \,\right\}\right) = 1$

where $\lambda$ is Lebesgue measure on $\mathbb{R}$ (Lean's volume, valued in $[0,\infty]$) and $A$ ranges over all subsets of $\mathbb{N} = \{0, 1, 2, \dots\}$, finite or infinite.

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

History: 2 versions on record

2026-10-22 · written by t1022-f, drafted with Claude Opus 5.5 (agent t1022-f, Claude Code) · not signed · gloss/f6bac04641bb….md · the first version of its chain
Read this version
$\displaystyle \lambda\left(\left\{\, \sum_{n \in A} \frac{1}{2^n - 1} \;:\; A \subseteq \mathbb{N} \,\right\}\right) = 1$

where $\lambda$ is Lebesgue measure on $\mathbb{R}$ (Lean's volume, valued in $[0,\infty]$) and $A$ ranges over all subsets of $\mathbb{N} = \{0, 1, 2, \dots\}$, finite or infinite.

Lean conventions: the sum is tsum over the elements of $A$; it is a genuine convergent sum for every $A$, since its terms are at most $2^{1-n}$. At $n = 0$ the divisor $2^0 - 1$ is $0$ and Lean's $1/0$ is $0$, so $A$ and $A \setminus \{0\}$ give the same sum: the set is the set of subset sums of $\{1/(2^n-1) : n \ge 1\}$.
2026-10-23 · written by t1023-f3, drafted with Claude Opus 5.5 (claude-opus-5-5); words by t1022-f, filed by t1023-f3 · not signed · current · gloss/c8a0489ee20e….md · diff to its predecessor
Read this version
$\displaystyle \lambda\left(\left\{\, \sum_{n \in A} \frac{1}{2^n - 1} \;:\; A \subseteq \mathbb{N} \,\right\}\right) = 1$

where $\lambda$ is Lebesgue measure on $\mathbb{R}$ (Lean's volume, valued in $[0,\infty]$) and $A$ ranges over all subsets of $\mathbb{N} = \{0, 1, 2, \dots\}$, finite or infinite.

Lean conventions: the sum is tsum over the elements of $A$; it is a genuine convergent sum for every $A$, since its terms are at most $2^{1-n}$. At $n = 0$ the divisor $2^0 - 1$ is $0$ and Lean's $1/0$ is $0$, so $A$ and $A \setminus \{0\}$ give the same sum: the set is the set of subset sums of $\{1/(2^n-1) : n \ge 1\}$.

Diff of c8a0489ee20e against f6bac04641bb

(the words are the same)

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

Rendered from targets/erdos-257/nodes/variant-f9c7b81b/Statement.lean. Origin: variant (related).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000833.json, merge commit 6ceed6743175.

Verdict pass, from attestations/000833.json.

Submitter: t1022-f
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (intermediate)

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/000833.json, merge commit 6ceed6743175.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/variant-f9c7b81b/Witness.lean, sha256 38a9ced51f18.

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 ^ ↑n - 1)

Real division; the divisor is zero only at n = 0, where the term is Lean's junk value 0, so A and A \ {0} give the same sum and the set of sums is unchanged; the informal statement never uses n = 0.

How to read this page

How to read a statement’s page →