Open Proof Network

Problems / erdos-257 / spec-a70fcca4--h2

no finite subsum is one half

spec-a70fcca4--h2 spec_a70fcca4__h2

proved

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

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

$\displaystyle \sum_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$

A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at $a = 0$ is Lean's $0$ and changes nothing), and one half is not. So any representation of one half by this series is infinite, which is what makes the greedy walk the only candidate.

unverified · history

Lean
theorem spec_a70fcca4__h2 : ∀ (S : Finset ℕ), ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≠ (1 / 2 : ℝ) := 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/088d62e9adb2….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_a = \frac{1}{2^a-1}$ (Lean's $t_0 = \frac10 = 0$). Every finite sum $\sum_{a\in S} t_a$ is a fraction $p/q$ of natural numbers with $q$ odd, because each $2^a - 1$ with $a \ge 1$ is odd and a product of odd numbers is odd. If such a sum were $\frac12$, then $q = 2p$ would be even. Contradiction.

Read it step by step (2 more sections)

Finite sums have odd denominators

Draft · drafted, by the model named above

By induction on the finite set $S$. For $S = \varnothing$ the sum is $0 = 0/1$. Adding a new element $a$ to $S$ whose sum is $p/q$ with $q$ odd: if $a = 0$ the new term is Lean's $0$ and nothing changes. If $a \ge 1$, then $d = 2^a - 1$ is odd ($2^a$ is even and $\ge 1$), it is nonzero, and as a real number it equals $2^a - 1$; so $$\frac{1}{2^a-1} + \frac pq \;=\; \frac{q + p\,d}{q\,d},$$ with $q\,d$ odd as a product of odd numbers.

One half is not such a fraction

Draft · drafted, by the model named above

Take $S$ with $\sum_{a\in S} t_a = \frac12$ and write the sum as $p/q$, $q$ odd (so $q \ne 0$). Clearing denominators in $p/q = \frac12$ gives $q = 2p$, first in $\mathbb{R}$ and then, casting back, in $\mathbb{N}$. So $q$ is even, contradicting that it is odd.

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

    Read this version

    Overview

    Write $t_a = \frac{1}{2^a-1}$ (Lean's $t_0 = \frac10 = 0$). Every finite sum $\sum_{a\in S} t_a$ is a fraction $p/q$ of natural numbers with $q$ odd, because each $2^a - 1$ with $a \ge 1$ is odd and a product of odd numbers is odd. If such a sum were $\frac12$, then $q = 2p$ would be even. Contradiction.

    Finite sums have odd denominators (key)

    By induction on the finite set $S$. For $S = \varnothing$ the sum is $0 = 0/1$. Adding a new element $a$ to $S$ whose sum is $p/q$ with $q$ odd: if $a = 0$ the new term is Lean's $0$ and nothing changes. If $a \ge 1$, then $d = 2^a - 1$ is odd ($2^a$ is even and $\ge 1$), it is nonzero, and as a real number it equals $2^a - 1$; so $$\frac{1}{2^a-1} + \frac pq \;=\; \frac{q + p\,d}{q\,d},$$ with $q\,d$ odd as a product of odd numbers.

    One half is not such a fraction (s2 hqne h2 h3 close)

    Take $S$ with $\sum_{a\in S} t_a = \frac12$ and write the sum as $p/q$, $q$ odd (so $q \ne 0$). Clearing denominators in $p/q = \frac12$ gives $q = 2p$, first in $\mathbb{R}$ and then, casting back, in $\mathbb{N}$. So $q$ is even, contradicting that it is odd.

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

The proof step by step (outline)

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

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. key have ∀ (S : Finset ℕ), ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ)

    Leaves ∀ (S : Finset ℕ), ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≠ (1 / 2 : ℝ), with key : ∀ (S : Finset ℕ), ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ).

    Uses library Finset Finset α is the type of finite sets of elements of α. , Odd An element a of a semiring is odd if there exists k such a = 2*k + 1. , Finset.induction_on To prove a proposition about an arbitrary Finset α, it suffices to prove it for the empty Finset, and to show that if it holds for some Finset α, then it holds for the Finset obtained by inserting a new element. .

    Lean, lines 8–28
      have key : ∀ S : Finset ℕ, ∃ p q : ℕ, Odd q ∧ ∑ a ∈ S, (1 : ℝ) / (2 ^ a - 1) = (p : ℝ) / q := by
    intro S
    induction S using Finset.induction_on with
    | empty => exact ⟨0, 1, odd_one, by simp⟩
    | insert a S ha ih =>
      obtain ⟨p, q, hq, hs⟩ := ih
      rw [Finset.sum_insert ha, hs]
      by_cases h0 : a = 0
      · subst h0
        exact ⟨p, q, hq, by simp⟩
      · have ha1 : 1 ≤ a := Nat.one_le_iff_ne_zero.mpr h0
        have hd : Odd (2 ^ a - 1) :=
          Nat.Even.sub_odd Nat.one_le_two_pow (Nat.even_pow.mpr ⟨even_two, h0⟩) odd_one
        have hdc : ((2 ^ a - 1 : ℕ) : ℝ) = 2 ^ a - 1 := by
          rw [Nat.cast_sub Nat.one_le_two_pow, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]
        have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'
        have hdne : ((2 ^ a - 1 : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hd.pos.ne'
        refine ⟨q + p * (2 ^ a - 1), q * (2 ^ a - 1), hq.mul hd, ?_⟩
        rw [← hdc]
        push_cast
        field_simp

    targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 8–28 at bdf809e0a538 ↗

    1. key.s1 case

      Leaves ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ ∅, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ).

      Uses library Finset.empty The empty finset , Exists.intro Existential introduction. , odd_one.

      Lean, line 11
          | empty => exact ⟨0, 1, odd_one, by simp⟩

      targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 11 at bdf809e0a538 ↗

    2. key.s2 case

      Leaves ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ insert a S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ), with a : ℕ, S : Finset ℕ, ha : a ∉ S, ih : ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ).

      Uses library Finset.sum_insert.

      Lean, lines 12–28
          | insert a S ha ih =>
      obtain ⟨p, q, hq, hs⟩ := ih
      rw [Finset.sum_insert ha, hs]
      by_cases h0 : a = 0
      · subst h0
        exact ⟨p, q, hq, by simp⟩
      · have ha1 : 1 ≤ a := Nat.one_le_iff_ne_zero.mpr h0
        have hd : Odd (2 ^ a - 1) :=
          Nat.Even.sub_odd Nat.one_le_two_pow (Nat.even_pow.mpr ⟨even_two, h0⟩) odd_one
        have hdc : ((2 ^ a - 1 : ℕ) : ℝ) = 2 ^ a - 1 := by
          rw [Nat.cast_sub Nat.one_le_two_pow, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]
        have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'
        have hdne : ((2 ^ a - 1 : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hd.pos.ne'
        refine ⟨q + p * (2 ^ a - 1), q * (2 ^ a - 1), hq.mul hd, ?_⟩
        rw [← hdc]
        push_cast
        field_simp

      targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 12–28 at bdf809e0a538 ↗

      1. key.s2.s1 obtain ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ)

        Leaves ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ insert a S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ), with p : ℕ, q : ℕ, hq : Odd q, hs : ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ).

        Lean, line 13
              obtain ⟨p, q, hq, hs⟩ := ih

        targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 13 at bdf809e0a538 ↗

      2. key.s2.s2 case

        Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with h0 : a = (0 : ℕ).

        Uses library Exists.intro Existential introduction. .

        Lean, lines 16–17
              · subst h0
        exact ⟨p, q, hq, by simp⟩

        targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 16–17 at bdf809e0a538 ↗

      3. key.s2.s3 case

        Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with h0 : ¬a = (0 : ℕ).

        Uses library Exists.intro Existential introduction. .

        Lean, lines 18–28
              · have ha1 : 1 ≤ a := Nat.one_le_iff_ne_zero.mpr h0
        have hd : Odd (2 ^ a - 1) :=
          Nat.Even.sub_odd Nat.one_le_two_pow (Nat.even_pow.mpr ⟨even_two, h0⟩) odd_one
        have hdc : ((2 ^ a - 1 : ℕ) : ℝ) = 2 ^ a - 1 := by
          rw [Nat.cast_sub Nat.one_le_two_pow, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]
        have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'
        have hdne : ((2 ^ a - 1 : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hd.pos.ne'
        refine ⟨q + p * (2 ^ a - 1), q * (2 ^ a - 1), hq.mul hd, ?_⟩
        rw [← hdc]
        push_cast
        field_simp

        targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 18–28 at bdf809e0a538 ↗

        1. key.s2.s3.ha1 have (1 : ℕ) ≤ a

          Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with ha1 : (1 : ℕ) ≤ a.

          Uses library Nat.one_le_iff_ne_zero.

          Lean, line 18
                · have ha1 : 1 ≤ a := Nat.one_le_iff_ne_zero.mpr h0

          targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 18 at bdf809e0a538 ↗

        2. key.s2.s3.hd have Odd ((2 : ℕ) ^ a - (1 : ℕ))

          Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with hd : Odd ((2 : ℕ) ^ a - (1 : ℕ)).

          Uses library Odd An element a of a semiring is odd if there exists k such a = 2*k + 1. , Nat.Even.sub_odd, Nat.one_le_two_pow, Nat.even_pow If m and n are natural numbers, then the natural number m^n is even if and only if m is even and n is positive. , And.intro And.intro : a → b → a ∧ b is the constructor for the And operation. , even_two, odd_one.

          Lean, lines 19–20
                  have hd : Odd (2 ^ a - 1) :=
          Nat.Even.sub_odd Nat.one_le_two_pow (Nat.even_pow.mpr ⟨even_two, h0⟩) odd_one

          targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 19–20 at bdf809e0a538 ↗

        3. key.s2.s3.hdc have (↑((2 : ℕ) ^ a - (1 : ℕ)) : ℝ) = (2 : ℝ) ^ a - (1 : ℝ)

          Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with hdc : (↑((2 : ℕ) ^ a - (1 : ℕ)) : ℝ) = (2 : ℝ) ^ a - (1 : ℝ).

          Uses library Nat.cast_sub, Nat.one_le_two_pow, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one.

          Lean, lines 21–22
                  have hdc : ((2 ^ a - 1 : ℕ) : ℝ) = 2 ^ a - 1 := by
          rw [Nat.cast_sub Nat.one_le_two_pow, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]

          targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 21–22 at bdf809e0a538 ↗

        4. key.s2.s3.hqne have (↑q : ℝ) ≠ (0 : ℝ)

          Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with hqne : (↑q : ℝ) ≠ (0 : ℝ).

          Uses library Nat.cast_ne_zero.

          Lean, line 23
                  have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'

          targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 23 at bdf809e0a538 ↗

        5. key.s2.s3.hdne have (↑((2 : ℕ) ^ a - (1 : ℕ)) : ℝ) ≠ (0 : ℝ)

          Leaves ∃ (p_1 : ℕ) (q_1 : ℕ), Odd q_1 ∧ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) + (↑p : ℝ) / (↑q : ℝ) = (↑p_1 : ℝ) / (↑q_1 : ℝ), with hdne : (↑((2 : ℕ) ^ a - (1 : ℕ)) : ℝ) ≠ (0 : ℝ).

          Uses library Nat.cast_ne_zero.

          Lean, line 24
                  have hdne : ((2 ^ a - 1 : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hd.pos.ne'

          targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 24 at bdf809e0a538 ↗

  2. s2 obtain ∃ (p : ℕ) (q : ℕ), Odd q ∧ ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ)

    Leaves False, with p : ℕ, q : ℕ, hq : Odd q, hs : ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) = (↑p : ℝ) / (↑q : ℝ).

    Lean, line 30
      obtain ⟨p, q, hq, hs⟩ := key S

    targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 30 at bdf809e0a538 ↗

  3. hqne have (↑q : ℝ) ≠ (0 : ℝ)

    Leaves False, with hqne : (↑q : ℝ) ≠ (0 : ℝ).

    Uses library Nat.cast_ne_zero.

    Lean, line 32
      have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'

    targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 32 at bdf809e0a538 ↗

  4. h2 have (↑q : ℝ) = (2 : ℝ) * (↑p : ℝ) routine: field_simp, linarith

    Leaves False, with h2 : (↑q : ℝ) = (2 : ℝ) * (↑p : ℝ).

    Lean, lines 33–35
      have h2 : (q : ℝ) = 2 * p := by
    field_simp at hS
    linarith

    targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, lines 33–35 at bdf809e0a538 ↗

  5. h3 have q = (2 : ℕ) * p

    Leaves False, with h3 : q = (2 : ℕ) * p.

    Lean, line 36
      have h3 : q = 2 * p := by exact_mod_cast h2

    targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 36 at bdf809e0a538 ↗

  6. close term False

    Closes the goal.

    Uses library Nat.not_even_iff_odd, Exists.intro Existential introduction. .

    Lean, line 37
      exact (Nat.not_even_iff_odd.mpr hq) ⟨p, by omega⟩

    targets/erdos-257/nodes/spec-a70fcca4--h2/Proof.lean, line 37 at bdf809e0a538 ↗

The proof in Lean (Proof.lean)

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

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--h2/Proof.lean, sha256 0cf1a869c11b.
import Mathlib
import Nodes.«spec-a70fcca4--h2».Context

/-! Hole `h2` 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__h2 : ∀ (S : Finset ℕ), ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≠ (1 / 2 : ℝ) := by
  have key : ∀ S : Finset ℕ, ∃ p q : ℕ, Odd q ∧ ∑ a ∈ S, (1 : ℝ) / (2 ^ a - 1) = (p : ℝ) / q := by
    intro S
    induction S using Finset.induction_on with
    | empty => exact ⟨0, 1, odd_one, by simp⟩
    | insert a S ha ih =>
      obtain ⟨p, q, hq, hs⟩ := ih
      rw [Finset.sum_insert ha, hs]
      by_cases h0 : a = 0
      · subst h0
        exact ⟨p, q, hq, by simp⟩
      · have ha1 : 1 ≤ a := Nat.one_le_iff_ne_zero.mpr h0
        have hd : Odd (2 ^ a - 1) :=
          Nat.Even.sub_odd Nat.one_le_two_pow (Nat.even_pow.mpr ⟨even_two, h0⟩) odd_one
        have hdc : ((2 ^ a - 1 : ℕ) : ℝ) = 2 ^ a - 1 := by
          rw [Nat.cast_sub Nat.one_le_two_pow, Nat.cast_pow, Nat.cast_ofNat, Nat.cast_one]
        have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'
        have hdne : ((2 ^ a - 1 : ℕ) : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hd.pos.ne'
        refine ⟨q + p * (2 ^ a - 1), q * (2 ^ a - 1), hq.mul hd, ?_⟩
        rw [← hdc]
        push_cast
        field_simp
  intro S hS
  obtain ⟨p, q, hq, hs⟩ := key S
  rw [hs] at hS
  have hqne : (q : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hq.pos.ne'
  have h2 : (q : ℝ) = 2 * p := by
    field_simp at hS
    linarith
  have h3 : q = 2 * p := by exact_mod_cast h2
  exact (Nat.not_even_iff_odd.mpr hq) ⟨p, by omega⟩

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 (3 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.«spec-a70fcca4--h2».Context

/-! Hole `h2` 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__h2 : ∀ (S : Finset ℕ), ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≠ (1 / 2 : ℝ) := 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_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$

A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at $a = 0$ is Lean's $0$ and changes nothing), and one half is not. So any representation of one half by this series is infinite, which is what makes the greedy walk the only candidate.

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

History: 3 versions on record

  1. 2026-10-20 · written by fable-1020-e257-b, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · gloss/2ab042c2c050….md · the first version of its chain

    Read this version

    $$\sum_{a\in S} \frac{1}{2^a-1} \ne \frac12$ for every finite $S \subseteq \mathbb{N}$$

    A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at a = 0 is Lean's 0), and 1/2 is not.

  2. 2026-10-20 · written by fable-1020-e257-b, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · gloss/7e2a50b953c4….md · diff to its predecessor

    Read this version

    $\displaystyle \sum_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$

    A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at $a = 0$ is Lean's $0$ and changes nothing), and one half is not. So any representation of one half by this series is infinite, which is what makes the greedy walk the only candidate.

  3. 2026-10-20 · written by fable-1020-e257-b, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/6a8be471540b….md · diff to its predecessor

    Read this version

    $\displaystyle \sum_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$

    A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at $a = 0$ is Lean's $0$ and changes nothing), and one half is not. So any representation of one half by this series is infinite, which is what makes the greedy walk the only candidate.

Diff of 7e2a50b953c4 against 2ab042c2c050
@@ -1,3 +1,3 @@
-$$\sum_{a\in S} \frac{1}{2^a-1} \ne \frac12$ for every finite $S \subseteq \mathbb{N}$$
+$$\sum_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$$
 
-A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at a = 0 is Lean's 0), and 1/2 is not.
+A finite sum of reciprocals of odd numbers is a rational with odd denominator (the term at $a = 0$ is Lean's $0$ and changes nothing), and one half is not. So any representation of one half by this series is infinite, which is what makes the greedy walk the only candidate.
Diff of 6a8be471540b against 7e2a50b953c4
(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/spec-a70fcca4--h2/Statement.lean. Origin: compiler-derived.

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000790.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/000790.json, merge commit bdf809e0a538.

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

theorem witness : ∃ S : Finset ℕ, 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 \exists\, S \subseteq \mathbb{N} \text{ finite}:\ \mathrm{True}$

The statement quantifies over a finite set $S$ (a Finset ℕ) with no hypothesis on it, so any finite set serves; the witness is the empty set.

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

How to read this page

How to read a statement’s page →