Open Proof Network

Problems / erdos-257 / spec-5e2e0890

subset sums determine the set (uniqueness)

spec-5e2e0890 Opn.erdos_257_subsum_injective

proved

Proposed by a contributor.

$\displaystyle A, B \subseteq \mathbb{N},\quad 0 \notin A,\quad 0 \notin B,\quad \sum_{n\in A}\frac{1}{2^n-1} \;=\; \sum_{n\in B}\frac{1}{2^n-1} \quad\Longrightarrow\quad A = B .$

The map $A \mapsto \sum_{n\in A} \frac{1}{2^n-1}$ is injective on sets of positive integers: a real number is the sum of at most one such set. The sums are Lean's tsum over the set; every such family is summable, so they are the ordinary sums. The hypotheses $0 \notin A$, $0 \notin B$ are needed in Lean: there $\frac{1}{2^0-1} = \frac10 = 0$, so $A$ and $A \cup \{0\}$ would have the same sum.

unverified · history

Lean
theorem Opn.erdos_257_subsum_injective (A B : Set ℕ) (hA : 0 ∉ A) (hB : 0 ∉ B)
    (h : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = ∑' n : B, (1 : ℝ) / (2 ^ n.1 - 1)) :
    A = B := 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

On the proof targets/erdos-257/nodes/spec-5e2e0890/Proof.lean:

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/7d18bad503ba….md, written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22.

Overview

Draft · drafted, by the model named above

Write $t_m = \frac{1}{2^m-1}$ (in Lean $t_0 = \frac10 = 0$). Suppose $0 \notin A$, $0 \notin B$ and $\sum_{a\in A} t_a = \sum_{b\in B} t_b$, but $A \ne B$. Let $n$ be the least element of the symmetric difference $A \,\triangle\, B$. Then $A$ and $B$ agree below $n$, $n \ge 1$ (since $0$ is in neither set), and the gap lemma spec-ddd99827 gives $\sum_{k\ge0} t_{n+1+k} < t_n$. The comparison lemma (hole spec-5e2e0890--h2) then says the set containing $n$ has the strictly larger sum, contradicting the equality.

Read it step by step (5 more sections)

The two facts taken from the holes

Draft · drafted, by the model named above

From the proved hole spec-5e2e0890--h1: the sequence $(t_m)_{m\ge0}$ is summable. From the proved hole spec-5e2e0890--h2, applied for a general $g$: if $g \ge 0$ is summable, $n \in S$, $n \notin T$, $S$ and $T$ agree on $\{0,\dots,n-1\}$, and $\sum_{k\ge0} g(n+1+k) < g(n)$, then $\sum_{m\in T} g(m) < \sum_{m\in S} g(m)$. Both holes are stated under the theorem's own hypotheses on $A$ and $B$, which is how the proof calls them.

The least point of difference

Draft · drafted, by the model named above

Arguing by contradiction from $A \ne B$: if no $n$ lay in exactly one of the sets, then $A = B$ by extensionality, so some $n$ lies in $A \setminus B$ or in $B \setminus A$. Take the least such $n$ (Nat.find). By minimality, every $m < n$ lies in both sets or in neither: $m \in A \iff m \in B$.

Nonnegativity of the terms

Draft · drafted, by the model named above

For every $m$, $2^m \ge 1$, so $2^m - 1 \ge 0$ and $t_m = \frac{1}{2^m-1} \ge 0$ (at $m=0$ this is Lean's $\frac10 = 0$).

The case n in A, not in B

Draft · drafted, by the model named above

Since $0 \notin A$ and $n \in A$, $n \ne 0$, so $n \ge 1$. Apply the comparison with $g = t$, $S = A$, $T = B$, using summability, nonnegativity, the agreement below $n$, and the gap lemma $\sum_{k\ge0} t_{n+1+k} < t_n$ at this $n \ge 1$. It gives $\sum_{b\in B} t_b < \sum_{a\in A} t_a$, contradicting the hypothesis that the two sums are equal.

The case n in B, not in A

Draft · drafted, by the model named above

Symmetric: $n \ge 1$ because $0 \notin B$, and the comparison with $S = B$, $T = A$ (agreement below $n$ read the other way round) gives $\sum_{a\in A} t_a < \sum_{b\in B} t_b$, again contradicting the equality. Hence $A = B$.

Improve these words →

History: 1 version on record

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

    Read this version

    Overview

    Write $t_m = \frac{1}{2^m-1}$ (in Lean $t_0 = \frac10 = 0$). Suppose $0 \notin A$, $0 \notin B$ and $\sum_{a\in A} t_a = \sum_{b\in B} t_b$, but $A \ne B$. Let $n$ be the least element of the symmetric difference $A \,\triangle\, B$. Then $A$ and $B$ agree below $n$, $n \ge 1$ (since $0$ is in neither set), and the gap lemma spec-ddd99827 gives $\sum_{k\ge0} t_{n+1+k} < t_n$. The comparison lemma (hole spec-5e2e0890--h2) then says the set containing $n$ has the strictly larger sum, contradicting the equality.

    The two facts taken from the holes (h1 h3)

    From the proved hole spec-5e2e0890--h1: the sequence $(t_m)_{m\ge0}$ is summable. From the proved hole spec-5e2e0890--h2, applied for a general $g$: if $g \ge 0$ is summable, $n \in S$, $n \notin T$, $S$ and $T$ agree on $\{0,\dots,n-1\}$, and $\sum_{k\ge0} g(n+1+k) < g(n)$, then $\sum_{m\in T} g(m) < \sum_{m\in S} g(m)$. Both holes are stated under the theorem's own hypotheses on $A$ and $B$, which is how the proof calls them.

    The least point of difference (hex hn hmin)

    Arguing by contradiction from $A \ne B$: if no $n$ lay in exactly one of the sets, then $A = B$ by extensionality, so some $n$ lies in $A \setminus B$ or in $B \setminus A$. Take the least such $n$ (Nat.find). By minimality, every $m < n$ lies in both sets or in neither: $m \in A \iff m \in B$.

    Nonnegativity of the terms (hnonneg)

    For every $m$, $2^m \ge 1$, so $2^m - 1 \ge 0$ and $t_m = \frac{1}{2^m-1} \ge 0$ (at $m=0$ this is Lean's $\frac10 = 0$).

    The case n in A, not in B (s7)

    Since $0 \notin A$ and $n \in A$, $n \ne 0$, so $n \ge 1$. Apply the comparison with $g = t$, $S = A$, $T = B$, using summability, nonnegativity, the agreement below $n$, and the gap lemma $\sum_{k\ge0} t_{n+1+k} < t_n$ at this $n \ge 1$. It gives $\sum_{b\in B} t_b < \sum_{a\in A} t_a$, contradicting the hypothesis that the two sums are equal.

    The case n in B, not in A (s8)

    Symmetric: $n \ge 1$ because $0 \notin B$, and the comparison with $S = B$, $T = A$ (agreement below $n$ read the other way round) gives $\sum_{a\in A} t_a < \sum_{b\in B} t_b$, again contradicting the equality. Hence $A = B$.

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

On the partial assembly targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean:

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/caef1e6d9c0b….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 assembly proves uniqueness of representation, $A = B$ whenever $0 \notin A$, $0 \notin B$ and $\sum_{n \in A} t_n = \sum_{n \in B} t_n$ with $t_n = \frac{1}{2^n - 1}$, from two holes and the gap lemma of spec-ddd99827, $\sum_{k \ge 0} t_{n+1+k} < t_n$ for $n \ge 1$ (Opn.erdos_257_tail_lt_term). Arguing by contradiction, it compares the two sums at the least element of the symmetric difference of $A$ and $B$.

Read it step by step (4 more sections)

The holes

Draft · drafted, by the model named above

Hole h1 (node spec-5e2e0890--h1): $(t_m)_{m \ge 0}$ is summable. Hole h3 (node spec-5e2e0890--h2): for $g \ge 0$ summable, sets $S, T$ and $n \in S \setminus T$ with $S$ and $T$ agreeing below $n$, if $\sum_{k \ge 0} g(n+1+k) < g(n)$ then $\sum_{m \in T} g(m) < \sum_{m \in S} g(m)$.

The least point of disagreement

Draft · drafted, by the model named above

If $A \ne B$, some $n$ lies in exactly one of them (hex, by extensionality). Let $n_0$ be the least such $n$ (Nat.find); it lies in exactly one of $A$, $B$ (hn), and every $m < n_0$ is in $A$ exactly when it is in $B$ (hmin, by minimality).

Nonnegativity

Draft · drafted, by the model named above

$2^m \ge 1$, so $t_m \ge 0$ for every $m$.

The two cases

Draft · drafted, by the model named above

If $n_0 \in A \setminus B$: since $0 \notin A$, $n_0 \ge 1$, so the gap lemma gives $\sum_{k} t_{n_0+1+k} < t_{n_0}$, and h3 with $g = t$, $S = A$, $T = B$ gives $\sum_{B} t < \sum_{A} t$, contradicting the equality of the sums. If $n_0 \in B \setminus A$, the same argument with the roles exchanged gives $\sum_{A} t < \sum_{B} t$.

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/caef1e6d9c0b….md · the first version of its chain

    Read this version

    Overview

    The assembly proves uniqueness of representation, $A = B$ whenever $0 \notin A$, $0 \notin B$ and $\sum_{n \in A} t_n = \sum_{n \in B} t_n$ with $t_n = \frac{1}{2^n - 1}$, from two holes and the gap lemma of spec-ddd99827, $\sum_{k \ge 0} t_{n+1+k} < t_n$ for $n \ge 1$ (Opn.erdos_257_tail_lt_term). Arguing by contradiction, it compares the two sums at the least element of the symmetric difference of $A$ and $B$.

    The holes (h1 h3)

    Hole h1 (node spec-5e2e0890--h1): $(t_m)_{m \ge 0}$ is summable. Hole h3 (node spec-5e2e0890--h2): for $g \ge 0$ summable, sets $S, T$ and $n \in S \setminus T$ with $S$ and $T$ agreeing below $n$, if $\sum_{k \ge 0} g(n+1+k) < g(n)$ then $\sum_{m \in T} g(m) < \sum_{m \in S} g(m)$.

    The least point of disagreement (hex hn hmin)

    If $A \ne B$, some $n$ lies in exactly one of them (hex, by extensionality). Let $n_0$ be the least such $n$ (Nat.find); it lies in exactly one of $A$, $B$ (hn), and every $m < n_0$ is in $A$ exactly when it is in $B$ (hmin, by minimality).

    Nonnegativity (hnonneg)

    $2^m \ge 1$, so $t_m \ge 0$ for every $m$.

    The two cases (s7 s8)

    If $n_0 \in A \setminus B$: since $0 \notin A$, $n_0 \ge 1$, so the gap lemma gives $\sum_{k} t_{n_0+1+k} < t_{n_0}$, and h3 with $g = t$, $S = A$, $T = B$ gives $\sum_{B} t < \sum_{A} t$, contradicting the equality of the sums. If $n_0 \in B \setminus A$, the same argument with the roles exchanged gives $\sum_{A} t < \sum_{B} t$.

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000793.json, merge commit 85a80f3ef0b4.

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. h1 have Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ))

    Leaves A = B, with h1 : Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)).

    Uses statements spec-5e2e0890--h1 spec_5e2e0890__h1; library Summable Summable f means that f has some (infinite) sum with respect to L. .

    Lean, line 20
      have h1 : Summable (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) := spec_5e2e0890__h1 A B hA hB h

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 20 at 85a80f3ef0b4 ↗

  2. h3 have ∀ (g : ℕ → ℝ), Summable g → (∀ (m : ℕ), (0 : ℝ) ≤ g m) → ∀ (S T : Set ℕ), ∀ n ∈ S, n ∉ T → (∀ m < n, m ∈ S ↔ m ∈ T) → ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n → ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ)

    Leaves A = B, with h3 : ∀ (g : ℕ → ℝ), Summable g → (∀ (m : ℕ), (0 : ℝ) ≤ g m) → ∀ (S T : Set ℕ), ∀ n ∈ S, n ∉ T → (∀ m < n, m ∈ S ↔ m ∈ T) → ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n → ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ).

    Uses statements spec-5e2e0890--h2 spec_5e2e0890__h2; library Summable Summable f means that f has some (infinite) sum with respect to L. , Set A set is a collection of elements of some type α. .

    Lean, lines 24–26
      have h3 : ∀ g : ℕ → ℝ, Summable g → (∀ m, 0 ≤ g m) → ∀ S T : Set ℕ, ∀ n : ℕ, n ∈ S → n ∉ T →
      (∀ m, m < n → (m ∈ S ↔ m ∈ T)) → ∑' k : ℕ, g (n + 1 + k) < g n →
      ∑' m : T, g m < ∑' m : S, g m := spec_5e2e0890__h2 A B hA hB h

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 24–26 at 85a80f3ef0b4 ↗

  3. hex have ∃ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A

    Leaves False, with hex : ∃ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A.

    Uses library Iff.intro If a → b and b → a then a and b are equivalent. .

    Lean, lines 29–34
      have hex : ∃ n, (n ∈ A ∧ n ∉ B) ∨ (n ∈ B ∧ n ∉ A) := by
    by_contra hno
    push_neg at hno
    apply hne
    ext m
    exact ⟨fun hm => (hno m).1 hm, fun hm => (hno m).2 hm⟩

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 29–34 at 85a80f3ef0b4 ↗

  4. hn have Nat.find hex ∈ A ∧ Nat.find hex ∉ B ∨ Nat.find hex ∈ B ∧ Nat.find hex ∉ A

    Leaves False, with hn : Nat.find hex ∈ A ∧ Nat.find hex ∉ B ∨ Nat.find hex ∈ B ∧ Nat.find hex ∉ A.

    Uses library Nat.find_spec.

    Lean, line 36
      have hn := Nat.find_spec hex

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 36 at 85a80f3ef0b4 ↗

  5. hmin have ∀ m < Nat.find hex, m ∈ A ↔ m ∈ B

    Leaves False, with hmin : ∀ m < Nat.find hex, m ∈ A ↔ m ∈ B.

    Uses library Nat.find If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. , Iff.intro If a → b and b → a then a and b are equivalent. .

    Lean, lines 37–41
      have hmin : ∀ m, m < Nat.find hex → (m ∈ A ↔ m ∈ B) := by
    intro m hm
    have hnot := Nat.find_min hex hm
    push_neg at hnot
    exact ⟨hnot.1, hnot.2⟩

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 37–41 at 85a80f3ef0b4 ↗

    1. hmin.hnot have ¬(m ∈ A ∧ m ∉ B ∨ m ∈ B ∧ m ∉ A)

      Leaves m ∈ A ↔ m ∈ B, with hnot : ¬(m ∈ A ∧ m ∉ B ∨ m ∈ B ∧ m ∉ A).

      Uses library Nat.find_min.

      Lean, line 39
          have hnot := Nat.find_min hex hm

      targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 39 at 85a80f3ef0b4 ↗

  6. hnonneg have ∀ (m : ℕ), (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ))

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

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

    Lean, lines 42–46
      have hnonneg : ∀ m : ℕ, (0 : ℝ) ≤ 1 / (2 ^ m - 1) := by
    intro m
    apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 42–46 at 85a80f3ef0b4 ↗

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

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

      Uses library one_le_pow₀.

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

      targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 45 at 85a80f3ef0b4 ↗

  7. s7 case

    Leaves False, with hnA : Nat.find hex ∈ A, hnB : Nat.find hex ∉ B.

    Uses library absurd Anything follows from two contradictory hypotheses. , ne_of_gt.

    Lean, lines 48–50
      · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_gt hlt)

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 48–50 at 85a80f3ef0b4 ↗

    1. s7.hn1 have (1 : ℕ) ≤ Nat.find hex

      Leaves False, with hn1 : (1 : ℕ) ≤ Nat.find hex.

      Uses library Nat.find If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. , Nat.one_le_iff_ne_zero.

      Lean, line 48
        · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))

      targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 48 at 85a80f3ef0b4 ↗

    2. s7.hlt have ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ))

      Leaves False, with hlt : ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)).

      Uses statements spec-ddd99827 Opn.erdos_257_tail_lt_term.

      Lean, line 49
          have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)

      targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 49 at 85a80f3ef0b4 ↗

  8. s8 case

    Leaves False, with hnB : Nat.find hex ∈ B, hnA : Nat.find hex ∉ A.

    Uses library absurd Anything follows from two contradictory hypotheses. , ne_of_lt.

    Lean, lines 51–54
      · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_lt hlt)

    targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 51–54 at 85a80f3ef0b4 ↗

    1. s8.hn1 have (1 : ℕ) ≤ Nat.find hex

      Leaves False, with hn1 : (1 : ℕ) ≤ Nat.find hex.

      Uses library Nat.find If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. , Nat.one_le_iff_ne_zero.

      Lean, line 51
        · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))

      targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, line 51 at 85a80f3ef0b4 ↗

    2. s8.hlt have ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ))

      Leaves False, with hlt : ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)).

      Uses statements spec-ddd99827 Opn.erdos_257_tail_lt_term.

      Lean, lines 52–53
          have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)

      targets/erdos-257/nodes/spec-5e2e0890/Proof.lean, lines 52–53 at 85a80f3ef0b4 ↗

The proof in Lean (Proof.lean)

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

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/Proof.lean, sha256 549e5e035a79.
import Mathlib
import Nodes.«spec-5e2e0890».Context
import Nodes.«spec-ddd99827».Proof

/-- Uniqueness of representation: two sets of positive integers with the same Mersenne
reciprocal sum are equal. It follows from the gap `∑_{m > n} 1/(2^m - 1) < 1/(2^n - 1)` by
looking at the least element of the symmetric difference. Consequence for Erdős 257: a rational
`x` is a subset sum for at most one `A`, found by the greedy walk (take `n` whenever the
remainder is at least `1/(2^n - 1)`), so the affirmative statement is false iff some rational
with an even denominator (such as `1/2`, whose representation cannot be finite) is reached by
a greedy walk that never stalls. -/
theorem Opn.erdos_257_subsum_injective (A B : Set ℕ) (hA : 0 ∉ A) (hB : 0 ∉ B)
    (h : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = ∑' n : B, (1 : ℝ) / (2 ^ n.1 - 1)) :
    A = B := by
  -- approach: least element of the symmetric difference; the side that contains it has the larger sum, by the gap lemma (spec-ddd99827, used)
  -- licence: CC-BY-4.0
  -- label: Mersenne reciprocals are summable
  -- claim: $\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$.
  have h1 : Summable (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) := spec_5e2e0890__h1 A B hA hB h
  -- label: lexicographic comparison of subset sums
  -- claim: $g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$
  -- Split both sums at $n$: the parts below $n$ agree, the $S$ side has $g(n)$ in addition, and the rest of the $T$ side is a tail bounded by the gap.
  have h3 : ∀ g : ℕ → ℝ, Summable g → (∀ m, 0 ≤ g m) → ∀ S T : Set ℕ, ∀ n : ℕ, n ∈ S → n ∉ T →
      (∀ m, m < n → (m ∈ S ↔ m ∈ T)) → ∑' k : ℕ, g (n + 1 + k) < g n →
      ∑' m : T, g m < ∑' m : S, g m := spec_5e2e0890__h2 A B hA hB h
  -- the assembly
  by_contra hne
  have hex : ∃ n, (n ∈ A ∧ n ∉ B) ∨ (n ∈ B ∧ n ∉ A) := by
    by_contra hno
    push_neg at hno
    apply hne
    ext m
    exact ⟨fun hm => (hno m).1 hm, fun hm => (hno m).2 hm⟩
  classical
  have hn := Nat.find_spec hex
  have hmin : ∀ m, m < Nat.find hex → (m ∈ A ↔ m ∈ B) := by
    intro m hm
    have hnot := Nat.find_min hex hm
    push_neg at hnot
    exact ⟨hnot.1, hnot.2⟩
  have hnonneg : ∀ m : ℕ, (0 : ℝ) ≤ 1 / (2 ^ m - 1) := by
    intro m
    apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith
  rcases hn with ⟨hnA, hnB⟩ | ⟨hnB, hnA⟩
  · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_gt hlt)
  · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_lt hlt)
How it was split
Split into

Proved from these holes by 20261020T203245Z-fable-1020-e257-a-partial.lean (merged in 379f92df0925, attestation 000782).

  • h1 → spec-5e2e0890--h1 (proved)

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

  • h3 → spec-5e2e0890--h2 (proved)

    $\displaystyle g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$

Read the partial proof (Lean)
theorem Opn.erdos_257_subsum_injective (A B : Set ℕ) (hA : 0 ∉ A) (hB : 0 ∉ B)
    (h : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = ∑' n : B, (1 : ℝ) / (2 ^ n.1 - 1)) :
    A = B := by
  -- approach: least element of the symmetric difference; the side that contains it has the larger sum, by the gap lemma (spec-ddd99827, used)
  -- licence: CC-BY-4.0
  -- label: Mersenne reciprocals are summable
  -- claim: $\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$.
  have h1 : Summable (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) := by sorry
  -- label: lexicographic comparison of subset sums
  -- claim: $g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$
  -- Split both sums at $n$: the parts below $n$ agree, the $S$ side has $g(n)$ in addition, and the rest of the $T$ side is a tail bounded by the gap.
  have h3 : ∀ g : ℕ → ℝ, Summable g → (∀ m, 0 ≤ g m) → ∀ S T : Set ℕ, ∀ n : ℕ, n ∈ S → n ∉ T →
      (∀ m, m < n → (m ∈ S ↔ m ∈ T)) → ∑' k : ℕ, g (n + 1 + k) < g n →
      ∑' m : T, g m < ∑' m : S, g m := by sorry
  -- the assembly: proved, not sorry
  by_contra hne
  have hex : ∃ n, (n ∈ A ∧ n ∉ B) ∨ (n ∈ B ∧ n ∉ A) := by
    by_contra hno
    push_neg at hno
    apply hne
    ext m
    exact ⟨fun hm => (hno m).1 hm, fun hm => (hno m).2 hm⟩
  classical
  have hn := Nat.find_spec hex
  have hmin : ∀ m, m < Nat.find hex → (m ∈ A ↔ m ∈ B) := by
    intro m hm
    have hnot := Nat.find_min hex hm
    push_neg at hnot
    exact ⟨hnot.1, hnot.2⟩
  have hnonneg : ∀ m : ℕ, (0 : ℝ) ≤ 1 / (2 ^ m - 1) := by
    intro m
    apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith
  rcases hn with ⟨hnA, hnB⟩ | ⟨hnB, hnA⟩
  · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_gt hlt)
  · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_lt hlt)

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean

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:00:23Z).

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/spec-5e2e0890/literature/20261022T130023Z-t1022-d.yaml.

Elementary and published (Kovač–Tao, Remark 4.1). Proved on this network.

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

/-- Uniqueness of representation: two sets of positive integers with the same Mersenne
reciprocal sum are equal. It follows from the gap `∑_{m > n} 1/(2^m - 1) < 1/(2^n - 1)` by
looking at the least element of the symmetric difference. Consequence for Erdős 257: a rational
`x` is a subset sum for at most one `A`, found by the greedy walk (take `n` whenever the
remainder is at least `1/(2^n - 1)`), so the affirmative statement is false iff some rational
with an even denominator (such as `1/2`, whose representation cannot be finite) is reached by
a greedy walk that never stalls. -/
theorem Opn.erdos_257_subsum_injective (A B : Set ℕ) (hA : 0 ∉ A) (hB : 0 ∉ B)
    (h : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = ∑' n : B, (1 : ℝ) / (2 ^ n.1 - 1)) :
    A = B := 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 t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle A, B \subseteq \mathbb{N},\quad 0 \notin A,\quad 0 \notin B,\quad \sum_{n\in A}\frac{1}{2^n-1} \;=\; \sum_{n\in B}\frac{1}{2^n-1} \quad\Longrightarrow\quad A = B .$

The map $A \mapsto \sum_{n\in A} \frac{1}{2^n-1}$ is injective on sets of positive integers: a real number is the sum of at most one such set. The sums are Lean's tsum over the set; every such family is summable, so they are the ordinary sums. The hypotheses $0 \notin A$, $0 \notin B$ are needed in Lean: there $\frac{1}{2^0-1} = \frac10 = 0$, so $A$ and $A \cup \{0\}$ would have the same sum.

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

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

Depends on (2), each in words

Depends on, each in words where someone has written them:

  • spec-5e2e0890--h1 spec_5e2e0890__h1: $\sum_{m \ge 0} \frac{1}{2^m - 1} < \infty \text{ (with Lean's convention } 1/0 = 0 \text{ at } m = 0)$ · used by the proof
  • spec-5e2e0890--h2 spec_5e2e0890__h2: $g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$ · used by the proof
Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000793.json, merge commit 85a80f3ef0b4.

Verdict pass, from attestations/000793.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/000793.json, merge commit 85a80f3ef0b4.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-257/nodes/spec-5e2e0890/Witness.lean, sha256 1bcf429d3aa0.
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 →

Attempts (1)

1 recorded. Routes refuted: none. Failure classes: none.

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by fable-1020-e257-a; merged in 379f92df0925 under attestations/000782.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean.

Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.

Outline of 20261020T203245Z-fable-1020-e257-a-partial.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. h1 hole Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) hole

    Leaves A = B, with h1 : Summable fun (m : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)).

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

    Left open as a hole; its statement is spec-5e2e0890--h1 spec_5e2e0890__h1 (proved).

    Lean, line 20
      have h1 : Summable (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) := by sorry

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 20 at 5fd58782b0c0 ↗

  2. h3 hole ∀ (g : ℕ → ℝ), Summable g → (∀ (m : ℕ), (0 : ℝ) ≤ g m) → ∀ (S T : Set ℕ), ∀ n ∈ S, n ∉ T → (∀ m < n, m ∈ S ↔ m ∈ T) → ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n → ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ) hole

    Leaves A = B, with h3 : ∀ (g : ℕ → ℝ), Summable g → (∀ (m : ℕ), (0 : ℝ) ≤ g m) → ∀ (S T : Set ℕ), ∀ n ∈ S, n ∉ T → (∀ m < n, m ∈ S ↔ m ∈ T) → ∑' (k : ℕ), g (n + (1 : ℕ) + k) < g n → ∑' (m : (↑T : Type)), g (↑m : ℕ) < ∑' (m : (↑S : Type)), g (↑m : ℕ).

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Set A set is a collection of elements of some type α. .

    Left open as a hole; its statement is spec-5e2e0890--h2 spec_5e2e0890__h2 (proved).

    Lean, lines 24–26
      have h3 : ∀ g : ℕ → ℝ, Summable g → (∀ m, 0 ≤ g m) → ∀ S T : Set ℕ, ∀ n : ℕ, n ∈ S → n ∉ T →
      (∀ m, m < n → (m ∈ S ↔ m ∈ T)) → ∑' k : ℕ, g (n + 1 + k) < g n →
      ∑' m : T, g m < ∑' m : S, g m := by sorry

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 24–26 at 5fd58782b0c0 ↗

  3. hex have ∃ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A

    Leaves False, with hex : ∃ (n : ℕ), n ∈ A ∧ n ∉ B ∨ n ∈ B ∧ n ∉ A.

    Uses library Iff.intro If a → b and b → a then a and b are equivalent. .

    Lean, lines 29–34
      have hex : ∃ n, (n ∈ A ∧ n ∉ B) ∨ (n ∈ B ∧ n ∉ A) := by
    by_contra hno
    push_neg at hno
    apply hne
    ext m
    exact ⟨fun hm => (hno m).1 hm, fun hm => (hno m).2 hm⟩

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 29–34 at 5fd58782b0c0 ↗

  4. hn have Nat.find hex ∈ A ∧ Nat.find hex ∉ B ∨ Nat.find hex ∈ B ∧ Nat.find hex ∉ A

    Leaves False, with hn : Nat.find hex ∈ A ∧ Nat.find hex ∉ B ∨ Nat.find hex ∈ B ∧ Nat.find hex ∉ A.

    Uses library Nat.find_spec.

    Lean, line 36
      have hn := Nat.find_spec hex

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 36 at 5fd58782b0c0 ↗

  5. hmin have ∀ m < Nat.find hex, m ∈ A ↔ m ∈ B

    Leaves False, with hmin : ∀ m < Nat.find hex, m ∈ A ↔ m ∈ B.

    Uses library Nat.find If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. , Iff.intro If a → b and b → a then a and b are equivalent. .

    Lean, lines 37–41
      have hmin : ∀ m, m < Nat.find hex → (m ∈ A ↔ m ∈ B) := by
    intro m hm
    have hnot := Nat.find_min hex hm
    push_neg at hnot
    exact ⟨hnot.1, hnot.2⟩

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 37–41 at 5fd58782b0c0 ↗

    1. hmin.hnot have ¬(m ∈ A ∧ m ∉ B ∨ m ∈ B ∧ m ∉ A)

      Leaves m ∈ A ↔ m ∈ B, with hnot : ¬(m ∈ A ∧ m ∉ B ∨ m ∈ B ∧ m ∉ A).

      Uses library Nat.find_min.

      Lean, line 39
          have hnot := Nat.find_min hex hm

      targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 39 at 5fd58782b0c0 ↗

  6. hnonneg have ∀ (m : ℕ), (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ))

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

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

    Lean, lines 42–46
      have hnonneg : ∀ m : ℕ, (0 : ℝ) ≤ 1 / (2 ^ m - 1) := by
    intro m
    apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 42–46 at 5fd58782b0c0 ↗

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

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

      Uses library one_le_pow₀.

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

      targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 45 at 5fd58782b0c0 ↗

  7. s7 case

    Leaves False, with hnA : Nat.find hex ∈ A, hnB : Nat.find hex ∉ B.

    Uses library absurd Anything follows from two contradictory hypotheses. , ne_of_gt.

    Lean, lines 48–50
      · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_gt hlt)

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 48–50 at 5fd58782b0c0 ↗

    1. s7.hn1 have (1 : ℕ) ≤ Nat.find hex

      Leaves False, with hn1 : (1 : ℕ) ≤ Nat.find hex.

      Uses library Nat.find If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. , Nat.one_le_iff_ne_zero.

      Lean, line 48
        · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))

      targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 48 at 5fd58782b0c0 ↗

    2. s7.hlt have ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ))

      Leaves False, with hlt : ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)).

      Uses statements spec-ddd99827 Opn.erdos_257_tail_lt_term.

      Lean, line 49
          have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)

      targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 49 at 5fd58782b0c0 ↗

  8. s8 case

    Leaves False, with hnB : Nat.find hex ∈ B, hnA : Nat.find hex ∉ A.

    Uses library absurd Anything follows from two contradictory hypotheses. , ne_of_lt.

    Lean, lines 51–54
      · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_lt hlt)

    targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 51–54 at 5fd58782b0c0 ↗

    1. s8.hn1 have (1 : ℕ) ≤ Nat.find hex

      Leaves False, with hn1 : (1 : ℕ) ≤ Nat.find hex.

      Uses library Nat.find If p is a (decidable) predicate on ℕ and hp : ∃ (n : ℕ), p n is a proof that there exists some natural number satisfying p, then Nat.find hp is the smallest natural number satisfying p. , Nat.one_le_iff_ne_zero.

      Lean, line 51
        · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))

      targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, line 51 at 5fd58782b0c0 ↗

    2. s8.hlt have ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ))

      Leaves False, with hlt : ∑' (m : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)) < ∑' (m : (↑B : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑m : ℕ) - (1 : ℝ)).

      Uses statements spec-ddd99827 Opn.erdos_257_tail_lt_term.

      Lean, lines 52–53
          have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)

      targets/erdos-257/nodes/spec-5e2e0890/attempts/20261020T203245Z-fable-1020-e257-a-partial.lean, lines 52–53 at 5fd58782b0c0 ↗

import Mathlib
import Nodes.«spec-5e2e0890».Context
import Nodes.«spec-ddd99827».Proof

/-- Uniqueness of representation: two sets of positive integers with the same Mersenne
reciprocal sum are equal. It follows from the gap `∑_{m > n} 1/(2^m - 1) < 1/(2^n - 1)` by
looking at the least element of the symmetric difference. Consequence for Erdős 257: a rational
`x` is a subset sum for at most one `A`, found by the greedy walk (take `n` whenever the
remainder is at least `1/(2^n - 1)`), so the affirmative statement is false iff some rational
with an even denominator (such as `1/2`, whose representation cannot be finite) is reached by
a greedy walk that never stalls. -/
theorem Opn.erdos_257_subsum_injective (A B : Set ℕ) (hA : 0 ∉ A) (hB : 0 ∉ B)
    (h : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = ∑' n : B, (1 : ℝ) / (2 ^ n.1 - 1)) :
    A = B := by
  -- approach: least element of the symmetric difference; the side that contains it has the larger sum, by the gap lemma (spec-ddd99827, used)
  -- licence: CC-BY-4.0
  -- label: Mersenne reciprocals are summable
  -- claim: $\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$.
  have h1 : Summable (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) := by sorry
  -- label: lexicographic comparison of subset sums
  -- claim: $g \ge 0 \text{ summable}, \sum_{k \ge 0} g(n+1+k) < g(n), n \in S \setminus T, S \cap [0,n) = T \cap [0,n) \implies \sum_{T} g < \sum_{S} g$
  -- Split both sums at $n$: the parts below $n$ agree, the $S$ side has $g(n)$ in addition, and the rest of the $T$ side is a tail bounded by the gap.
  have h3 : ∀ g : ℕ → ℝ, Summable g → (∀ m, 0 ≤ g m) → ∀ S T : Set ℕ, ∀ n : ℕ, n ∈ S → n ∉ T →
      (∀ m, m < n → (m ∈ S ↔ m ∈ T)) → ∑' k : ℕ, g (n + 1 + k) < g n →
      ∑' m : T, g m < ∑' m : S, g m := by sorry
  -- the assembly: proved, not sorry
  by_contra hne
  have hex : ∃ n, (n ∈ A ∧ n ∉ B) ∨ (n ∈ B ∧ n ∉ A) := by
    by_contra hno
    push_neg at hno
    apply hne
    ext m
    exact ⟨fun hm => (hno m).1 hm, fun hm => (hno m).2 hm⟩
  classical
  have hn := Nat.find_spec hex
  have hmin : ∀ m, m < Nat.find hex → (m ∈ A ↔ m ∈ B) := by
    intro m hm
    have hnot := Nat.find_min hex hm
    push_neg at hnot
    exact ⟨hnot.1, hnot.2⟩
  have hnonneg : ∀ m : ℕ, (0 : ℝ) ≤ 1 / (2 ^ m - 1) := by
    intro m
    apply div_nonneg zero_le_one
    have : (1 : ℝ) ≤ 2 ^ m := one_le_pow₀ (by norm_num)
    linarith
  rcases hn with ⟨hnA, hnB⟩ | ⟨hnB, hnA⟩
  · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hA (h0 ▸ hnA))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg A B _ hnA hnB hmin (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_gt hlt)
  · have hn1 : 1 ≤ Nat.find hex := Nat.one_le_iff_ne_zero.mpr (fun h0 => hB (h0 ▸ hnB))
    have hlt := h3 (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) h1 hnonneg B A _ hnB hnA
      (fun m hm => (hmin m hm).symm) (Opn.erdos_257_tail_lt_term _ hn1)
    exact absurd h (ne_of_lt hlt)
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; both sets exclude 0 by hypothesis, so every divisor 2^n - 1 is positive, and the junk value at n = 0 is exactly what the hypotheses 0 ∉ A, 0 ∉ B rule out (without them the statement is false: A and A ∪ {0} have equal sums).

How to read this page

How to read a statement’s page →