Open Proof Network

Problems / erdos-257 / spec-a70fcca4

spec-a70fcca4 Opn.erdos_257_half_is_a_subsum

superseded

Proposed by a contributor.

Superseded by spec-a70fcca4-v2. Work continues on the replacement; this statement is kept for its history (D-8). The curator's record: superseded by spec-a70fcca4-v2 on revision request targets/erdos-257/nodes/spec-a70fcca4/revisions/20261021T120000Z-thisisanameforsure.yaml (other-with-exhibit; D-8)

theorem Opn.erdos_257_half_is_a_subsum :
    ∃ A : Set ℕ, A.Infinite ∧ ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 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 →

Explain this →

Explainer

On the partial assembly targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-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/f803a0ad9ba0….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

The claim is that $\frac12 = \sum_{a\in A} t_a$ for an infinite $A$, where $t_a = \frac{1}{2^a-1}$ (Lean's $t_0 = \frac10 = 0$). The partial proof runs the greedy walk for $\frac12$: $r_0 = \frac12$, and $r_{m+1} = r_m - t_m$ if $t_m \le r_m$, else $r_{m+1} = r_m$; $A$ is the set of positions the walk takes. Granting four statements (the holes), it shows $r_m \to 0$, hence $\sum_{a\in A} t_a = \frac12$, and that $A$ is infinite because no finite sum of the $t_a$ is $\frac12$. Only the fourth hole, that the walk never stalls, is open; the assembly below is checked by the kernel.

Read it step by step (6 more sections)

The four holes

Draft · drafted, by the model named above

Each hole is stated for an arbitrary $r$ satisfying the walk's recursion, so each is a statement of its own.

  • h1 (spec-a70fcca4--h1, proved): for every $m$, $r_m \ge 0$ and the sum of the taken terms below $m$ is $\frac12 - r_m$.
  • h2 (spec-a70fcca4--h2, proved): $\sum_{a\in S} t_a \ne \frac12$ for every finite $S \subseteq \mathbb{N}$.
  • h3 (spec-a70fcca4--h3, proved): $(t_n)$ is summable. The assembly below does not refer to h3: the tail-to-zero step (tendsto_sum_nat_add) is applied to the sequence with no summability argument.
  • h4 (spec-a70fcca4--h4, open): for every $m$, $r_m \le \sum_{k\ge0} t_{k+m}$, the whole tail from $m$ on: the walk never stalls.

The walk exists

Draft · drafted, by the model named above

The sequence $r$ is defined by recursion on $m$ with exactly the recursion above, so it exists; the proof fixes it and specialises h1 and h4 to it.

The remainder tends to zero

Draft · drafted, by the model named above

The tails $\sum_{k\ge0} t_{k+m}$ tend to $0$ as $m \to \infty$. Since $0 \le r_m$ (h1) and $r_m \le \sum_{k\ge0} t_{k+m}$ (h4), the squeeze gives $r_m \to 0$.

The taken terms sum to one half

Draft · drafted, by the model named above

Let $f(a) = t_a$ if $t_a \le r_a$ (position $a$ is taken) and $f(a) = 0$ otherwise. Every $f(a) \ge 0$. By h1, $\sum_{a<m} f(a) = \frac12 - r_m \to \frac12$. For a nonnegative sequence, convergence of the partial sums is the sum, so $\sum_{a\ge0} f(a) = \frac12$.

The taken set is infinite

Draft · drafted, by the model named above

Take $A = \{a : t_a \le r_a\}$ and suppose it is finite, bounded by $M$. For $a > M$ nothing is taken, so the walk is constant from $M+1$ on: $r_a = r_{M+1}$ for all $a \ge M+1$, by induction on $a$. A constant sequence tends to its value, and $r_m \to 0$, so $r_{M+1} = 0$. Then h1 at $M+1$ says the taken terms below $M+1$ sum to exactly $\frac12$, a finite subsum equal to $\frac12$, which h2 forbids.

The sum over the taken set is one half

Draft · drafted, by the model named above

The sum of $t$ over the set $A$ equals the sum over all $a$ of the indicator of $A$ times $t$, and that indicator function is $f$. So $\sum_{a\in A} t_a = \sum_a f(a) = \frac12$.

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

    Read this version

    Overview

    The claim is that $\frac12 = \sum_{a\in A} t_a$ for an infinite $A$, where $t_a = \frac{1}{2^a-1}$ (Lean's $t_0 = \frac10 = 0$). The partial proof runs the greedy walk for $\frac12$: $r_0 = \frac12$, and $r_{m+1} = r_m - t_m$ if $t_m \le r_m$, else $r_{m+1} = r_m$; $A$ is the set of positions the walk takes. Granting four statements (the holes), it shows $r_m \to 0$, hence $\sum_{a\in A} t_a = \frac12$, and that $A$ is infinite because no finite sum of the $t_a$ is $\frac12$. Only the fourth hole, that the walk never stalls, is open; the assembly below is checked by the kernel.

    The four holes (h1 h2 h3 h4)

    Each hole is stated for an arbitrary $r$ satisfying the walk's recursion, so each is a statement of its own.

    • h1 (spec-a70fcca4--h1, proved): for every $m$, $r_m \ge 0$ and the sum of the taken terms below $m$ is $\frac12 - r_m$.
    • h2 (spec-a70fcca4--h2, proved): $\sum_{a\in S} t_a \ne \frac12$ for every finite $S \subseteq \mathbb{N}$.
    • h3 (spec-a70fcca4--h3, proved): $(t_n)$ is summable. The assembly below does not refer to h3: the tail-to-zero step (tendsto_sum_nat_add) is applied to the sequence with no summability argument.
    • h4 (spec-a70fcca4--h4, open): for every $m$, $r_m \le \sum_{k\ge0} t_{k+m}$, the whole tail from $m$ on: the walk never stalls.

    The walk exists (hex s6)

    The sequence $r$ is defined by recursion on $m$ with exactly the recursion above, so it exists; the proof fixes it and specialises h1 and h4 to it.

    The remainder tends to zero (htail hr)

    The tails $\sum_{k\ge0} t_{k+m}$ tend to $0$ as $m \to \infty$. Since $0 \le r_m$ (h1) and $r_m \le \sum_{k\ge0} t_{k+m}$ (h4), the squeeze gives $r_m \to 0$.

    The taken terms sum to one half (hfnn hpart hsum)

    Let $f(a) = t_a$ if $t_a \le r_a$ (position $a$ is taken) and $f(a) = 0$ otherwise. Every $f(a) \ge 0$. By h1, $\sum_{a<m} f(a) = \frac12 - r_m \to \frac12$. For a nonnegative sequence, convergence of the partial sums is the sum, so $\sum_{a\ge0} f(a) = \frac12$.

    The taken set is infinite (s12)

    Take $A = \{a : t_a \le r_a\}$ and suppose it is finite, bounded by $M$. For $a > M$ nothing is taken, so the walk is constant from $M+1$ on: $r_a = r_{M+1}$ for all $a \ge M+1$, by induction on $a$. A constant sequence tends to its value, and $r_m \to 0$, so $r_{M+1} = 0$. Then h1 at $M+1$ says the taken terms below $M+1$ sum to exactly $\frac12$, a finite subsum equal to $\frac12$, which h2 forbids.

    The sum over the taken set is one half (s13)

    The sum of $t$ over the set $A$ equals the sum over all $a$ of the indicator of $A$ times $t$, and that indicator function is $f$. So $\sum_{a\in A} t_a = \sum_a f(a) = \frac12$.

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 is being proved

Superseded.

Split into

Proved from these holes by 20261020T203100Z-fable-1020-e257-b-partial.lean (merged in 3e74589bdca4, attestation 000783).

  • h1 → spec-a70fcca4--h1 (proved)

    $\displaystyle \forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$

  • h2 → spec-a70fcca4--h2 (proved)

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

  • h3 → spec-a70fcca4--h3 (proved)

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

  • h4 → spec-a70fcca4--h4 (open)

    $\displaystyle \forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ r_m\le\sum_{k=0}^{\infty}\frac{1}{2^{k+m}-1}.$

Read the partial proof (Lean)
theorem Opn.erdos_257_half_is_a_subsum :
    ∃ A : Set ℕ, A.Infinite ∧ ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = 1 / 2 := by
  -- approach: the greedy walk for 1/2 (take 1/(2^m-1) whenever it fits under the remainder r m); the bookkeeping is three provable holes and the open mathematics is one hole, that the walk never stalls
  -- licence: CC-BY-4.0
  -- The greedy remainder r : ℕ → ℝ has r 0 = 1/2, and position m is taken iff its term fits
  -- under r m. (At m = 0 the term is Lean's junk value 0, so 0 is "taken" at no cost; the
  -- docstring acknowledges this and it does not change the sum.) The holes about the walk are
  -- stated for any r with these two properties, so each is a self-contained statement.
  -- label: greedy remainder bookkeeping
  -- claim: $0 \le r_m$ and $\sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m$ for every $m$, where $A=\{a : \frac{1}{2^a-1}\le r_a\}$
  -- The remainder never goes negative (a term is subtracted only when it fits) and is exactly
  -- 1/2 minus the sum of the terms taken so far. Induction on m.
  have h1 : ∀ r : ℕ → ℝ, r 0 = 1 / 2 →
      (∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) →
      ∀ m, 0 ≤ r m ∧
        ∑ a ∈ Finset.range m, (if (1 : ℝ) / (2 ^ a - 1) ≤ r a then (1 : ℝ) / (2 ^ a - 1) else 0)
          = 1 / 2 - r m := sorry
  -- label: no finite subsum is one half
  -- claim: $\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.
  have h2 : ∀ S : Finset ℕ, ∑ a ∈ S, (1 : ℝ) / (2 ^ a - 1) ≠ 1 / 2 := sorry
  -- label: the Mersenne reciprocal series converges
  -- claim: $\sum_{n\ge 0} \frac{1}{2^n-1} < \infty$
  -- (summable; the n = 0 term is Lean's 0.)
  -- Comparison with the geometric series: 1/(2^n-1) ≤ 2/2^n for n ≥ 1.
  have h3 : Summable (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) := sorry
  -- label: the greedy walk for one half never stalls
  -- claim: $r_m \le \sum_{k\ge 0} \frac{1}{2^{k+m}-1}$ for every $m$, for the greedy remainder $r$ of $\frac12$
  -- The open mathematics. The remainder before position m never exceeds the whole tail of the
  -- series from m on, so the walk can always continue; equivalently (given the holes above) the
  -- remainder tends to 0. Verified numerically to depth 10^8 (Hong 2026), no proof known. A
  -- stall at m would be r m > tail m, after which 1/2 is not a subset sum at all.
  have h4 : ∀ r : ℕ → ℝ, r 0 = 1 / 2 →
      (∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) →
      ∀ m, r m ≤ ∑' k : ℕ, (1 : ℝ) / (2 ^ (k + m) - 1) := sorry
  -- The walk itself, by recursion on m.
  have hex : ∃ r : ℕ → ℝ, r 0 = 1 / 2 ∧
      ∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m :=
    ⟨fun m => Nat.rec (1 / 2 : ℝ)
        (fun k rk => if (1 : ℝ) / (2 ^ k - 1) ≤ rk then rk - 1 / (2 ^ k - 1) else rk) m,
      rfl, fun _ => rfl⟩
  obtain ⟨r, hr0, hrs⟩ := hex
  replace h1 := h1 r hr0 hrs
  replace h4 := h4 r hr0 hrs
  -- The assembly. Tail of a convergent series tends to 0, so r m → 0 by the squeeze.
  have htail : Filter.Tendsto (fun m : ℕ => ∑' k : ℕ, (1 : ℝ) / (2 ^ (k + m) - 1))
      Filter.atTop (nhds 0) := tendsto_sum_nat_add (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))
  have hr : Filter.Tendsto r Filter.atTop (nhds 0) :=
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds htail (fun m => (h1 m).1) h4
  -- The partial sums of the chosen terms tend to 1/2.
  set f : ℕ → ℝ := fun a => if (1 : ℝ) / (2 ^ a - 1) ≤ r a then (1 : ℝ) / (2 ^ a - 1) else 0
    with hf
  have hfnn : ∀ a, 0 ≤ f a := by
    intro a
    simp only [hf]
    split_ifs with h
    · have h2a : (1 : ℝ) ≤ 2 ^ a := one_le_pow₀ (by norm_num)
      exact div_nonneg zero_le_one (by linarith)
    · exact le_refl 0
  have hpart : Filter.Tendsto (fun m => ∑ a ∈ Finset.range m, f a) Filter.atTop (nhds (1 / 2)) := by
    have : (fun m => ∑ a ∈ Finset.range m, f a) = fun m => 1 / 2 - r m := by
      funext m; exact (h1 m).2
    rw [this]
    simpa using tendsto_const_nhds.sub hr
  have hsum : HasSum f (1 / 2) := (hasSum_iff_tendsto_nat_of_nonneg hfnn _).mpr hpart
  refine ⟨{a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a}, ?_, ?_⟩
  · -- Infinite: if A were finite the walk would be constant from some M on, so r M = 0 by hr,
    -- and 1/2 would be the finite sum of the terms taken below M, against h2.
    intro hfin
    obtain ⟨M, hM⟩ := hfin.bddAbove
    have hconst : ∀ a, M + 1 ≤ a → r a = r (M + 1) := by
      intro a ha
      induction a, ha using Nat.le_induction with
      | base => rfl
      | succ a ha ih =>
        rw [hrs a, if_neg, ih]
        intro hle
        exact absurd (hM hle) (by omega)
    have hc : Filter.Tendsto r Filter.atTop (nhds (r (M + 1))) := by
      refine tendsto_const_nhds.congr' ?_
      filter_upwards [Filter.eventually_ge_atTop (M + 1)] with a ha
      exact (hconst a ha).symm
    have hzero : r (M + 1) = 0 := tendsto_nhds_unique hc hr
    have hhalf := (h1 (M + 1)).2
    rw [hzero, sub_zero] at hhalf
    apply h2 ((Finset.range (M + 1)).filter fun a => (1 : ℝ) / (2 ^ a - 1) ≤ r a)
    rw [Finset.sum_filter]
    exact hhalf
  · -- The sum over A is the sum of f.
    have hind : (Set.indicator {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) = f := by
      funext a
      simp only [Set.indicator_apply, Set.mem_setOf_eq, hf]
    refine (tsum_subtype {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)).trans ?_
    rw [hind]
    exact hsum.tsum_eq

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

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 no words yet

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

/-- The natural counterexample candidate for Erdős 257, stated so that it can be proved or
refuted: `1/2` is the Mersenne reciprocal sum of some infinite set. A finite set cannot give
`1/2` (finite sums have odd denominators), so any representation of `1/2` is infinite, and a
proof of this statement refutes the root. The greedy walk for `1/2` (the only possible
representation) begins 2, 3, 6, 7, 14, 20, 21, 26, 27, 32, ... and has been run without stalling
to depth 2500 here and to depth 10^8 by Hong (Zenodo 23287959, 2026, unrefereed); Kovač
(erdosproblems.com/257, Aug 2025) expects the subset-sum set, a fat Cantor set, to contain
such rationals. No proof in either direction is known. -/
theorem Opn.erdos_257_half_is_a_subsum :
    ∃ A : Set ℕ, A.Infinite ∧ ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 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 →

No gloss yet: no one has written in words what this statement says (D-3 v3.30); the Lean above is the statement. How to write one →

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

Depends on (4), each in words

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

  • spec-a70fcca4--h1 spec_a70fcca4__h1: $\forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ \ 0\le r_m \ \text{ and } \sum_{\substack{a<m\\ \frac{1}{2^a-1}\le r_a}}\frac{1}{2^a-1}=\frac12-r_m .$
  • spec-a70fcca4--h2 spec_a70fcca4__h2: $\sum_{a\in S} \frac{1}{2^a-1} \ne \frac12 \quad\text{for every finite } S \subseteq \mathbb{N}.$
  • spec-a70fcca4--h3 spec_a70fcca4__h3: $\sum_{n\ge 0} \frac{1}{2^n-1} < \infty$
  • spec-a70fcca4--h4 spec_a70fcca4__h4: $\forall\, r:\mathbb{N}\to\mathbb{R}:\quad r_0=\tfrac12,\ \ \forall m:\ r_{m+1}=\begin{cases} r_m-\dfrac{1}{2^m-1} & \text{if } \dfrac{1}{2^m-1}\le r_m,\\[4pt] r_m & \text{otherwise}\end{cases} \ \Longrightarrow\ \forall m:\ r_m\le\sum_{k=0}^{\infty}\frac{1}{2^{k+m}-1}.$
Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000783.json: it records an attempt, not a proof (see Attempts below).

Witness

Not checked — no run on this page records step 7 passing for it.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-257/nodes/spec-a70fcca4/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 →

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-b; merged in 3e74589bdca4 under attestations/000783.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-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-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 20261020T203100Z-fable-1020-e257-b-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 ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), (0 : ℝ) ≤ r m ∧ (∑ a ∈ Finset.range m, if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r m hole

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with h1 : ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), (0 : ℝ) ≤ r m ∧ (∑ a ∈ Finset.range m, if (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a then (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) else (0 : ℝ)) = (1 / 2 : ℝ) - r m.

    Uses library Finset.range range n is the set of natural numbers less than n. .

    Left open as a hole; its statement is spec-a70fcca4--h1 spec_a70fcca4__h1 (proved).

    Lean, lines 24–28
      have h1 : ∀ r : ℕ → ℝ, r 0 = 1 / 2 →
      (∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) →
      ∀ m, 0 ≤ r m ∧
        ∑ a ∈ Finset.range m, (if (1 : ℝ) / (2 ^ a - 1) ≤ r a then (1 : ℝ) / (2 ^ a - 1) else 0)
          = 1 / 2 - r m := sorry

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 24–28 at 60a537454ac8 ↗

  2. h2 hole ∀ (S : Finset ℕ), ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≠ (1 / 2 : ℝ) hole

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with h2 : ∀ (S : Finset ℕ), ∑ a ∈ S, (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≠ (1 / 2 : ℝ).

    Uses library Finset Finset α is the type of finite sets of elements of α. .

    Left open as a hole; its statement is spec-a70fcca4--h2 spec_a70fcca4__h2 (proved).

    Lean, line 33
      have h2 : ∀ S : Finset ℕ, ∑ a ∈ S, (1 : ℝ) / (2 ^ a - 1) ≠ 1 / 2 := sorry

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 33 at 60a537454ac8 ↗

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

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with h3 : Summable fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (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-a70fcca4--h3 spec_a70fcca4__h3 (proved).

    Lean, line 38
      have h3 : Summable (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) := sorry

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 38 at 60a537454ac8 ↗

  4. h4 hole ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), r m ≤ ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (k + m) - (1 : ℝ)) hole

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with h4 : ∀ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) → (∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m) → ∀ (m : ℕ), r m ≤ ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (k + m) - (1 : ℝ)).

    Left open as a hole; its statement is spec-a70fcca4--h4 spec_a70fcca4__h4 (open).

    Lean, lines 45–47
      have h4 : ∀ r : ℕ → ℝ, r 0 = 1 / 2 →
      (∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) →
      ∀ m, r m ≤ ∑' k : ℕ, (1 : ℝ) / (2 ^ (k + m) - 1) := sorry

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 45–47 at 60a537454ac8 ↗

  5. hex have ∃ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) ∧ ∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with hex : ∃ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) ∧ ∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m.

    Uses library Exists.intro Existential introduction. , Nat.rec, rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 49–53
      have hex : ∃ r : ℕ → ℝ, r 0 = 1 / 2 ∧
      ∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m :=
    ⟨fun m => Nat.rec (1 / 2 : ℝ)
        (fun k rk => if (1 : ℝ) / (2 ^ k - 1) ≤ rk then rk - 1 / (2 ^ k - 1) else rk) m,
      rfl, fun _ => rfl⟩

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 49–53 at 60a537454ac8 ↗

  6. s6 obtain ∃ (r : ℕ → ℝ), r (0 : ℕ) = (1 / 2 : ℝ) ∧ ∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with r : ℕ → ℝ, hr0 : r (0 : ℕ) = (1 / 2 : ℝ), hrs : ∀ (m : ℕ), r (m + (1 : ℕ)) = if (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) ≤ r m then r m - (1 : ℝ) / ((2 : ℝ) ^ m - (1 : ℝ)) else r m.

    Lean, line 54
      obtain ⟨r, hr0, hrs⟩ := hex

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 54 at 60a537454ac8 ↗

  7. htail have Filter.Tendsto (fun (m : ℕ) => ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (k + m) - (1 : ℝ))) Filter.atTop (nhds (0 : ℝ))

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with htail : Filter.Tendsto (fun (m : ℕ) => ∑' (k : ℕ), (1 : ℝ) / ((2 : ℝ) ^ (k + m) - (1 : ℝ))) Filter.atTop (nhds (0 : ℝ)).

    Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , tendsto_sum_nat_add For f : ℕ → G, the sum ∑' k, f (k + i) tends to zero. .

    Lean, lines 58–59
      have htail : Filter.Tendsto (fun m : ℕ => ∑' k : ℕ, (1 : ℝ) / (2 ^ (k + m) - 1))
      Filter.atTop (nhds 0) := tendsto_sum_nat_add (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 58–59 at 60a537454ac8 ↗

  8. hr have Filter.Tendsto r Filter.atTop (nhds (0 : ℝ))

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with hr : Filter.Tendsto r Filter.atTop (nhds (0 : ℝ)).

    Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , tendsto_of_tendsto_of_tendsto_of_le_of_le Squeeze theorem (also known as sandwich theorem). , tendsto_const_nhds.

    Lean, lines 60–61
      have hr : Filter.Tendsto r Filter.atTop (nhds 0) :=
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds htail (fun m => (h1 m).1) h4

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 60–61 at 60a537454ac8 ↗

  9. hfnn have ∀ (a : ℕ), (0 : ℝ) ≤ f a

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with hfnn : ∀ (a : ℕ), (0 : ℝ) ≤ f a.

    Lean, lines 65–71
      have hfnn : ∀ a, 0 ≤ f a := by
    intro a
    simp only [hf]
    split_ifs with h
    · have h2a : (1 : ℝ) ≤ 2 ^ a := one_le_pow₀ (by norm_num)
      exact div_nonneg zero_le_one (by linarith)
    · exact le_refl 0

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 65–71 at 60a537454ac8 ↗

    1. hfnn.s1 case

      Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)), with h : (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a.

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

      Lean, lines 69–70
          · have h2a : (1 : ℝ) ≤ 2 ^ a := one_le_pow₀ (by norm_num)
      exact div_nonneg zero_le_one (by linarith)

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 69–70 at 60a537454ac8 ↗

      1. hfnn.s1.h2a have (1 : ℝ) ≤ (2 : ℝ) ^ a

        Leaves (0 : ℝ) ≤ (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)), with h2a : (1 : ℝ) ≤ (2 : ℝ) ^ a.

        Uses library one_le_pow₀.

        Lean, line 69
            · have h2a : (1 : ℝ) ≤ 2 ^ a := one_le_pow₀ (by norm_num)

        targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 69 at 60a537454ac8 ↗

    2. hfnn.s2 case

      Leaves (0 : ℝ) ≤ (0 : ℝ), with h : ¬(1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a.

      Uses library le_refl The relation ≤ on a preorder is reflexive. .

      Lean, line 71
          · exact le_refl 0

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 71 at 60a537454ac8 ↗

  10. hpart have Filter.Tendsto (fun (m : ℕ) => ∑ a ∈ Finset.range m, f a) Filter.atTop (nhds (1 / 2 : ℝ))

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with hpart : Filter.Tendsto (fun (m : ℕ) => ∑ a ∈ Finset.range m, f a) Filter.atTop (nhds (1 / 2 : ℝ)).

    Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , Finset.range range n is the set of natural numbers less than n. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , tendsto_const_nhds.

    Lean, lines 72–76
      have hpart : Filter.Tendsto (fun m => ∑ a ∈ Finset.range m, f a) Filter.atTop (nhds (1 / 2)) := by
    have : (fun m => ∑ a ∈ Finset.range m, f a) = fun m => 1 / 2 - r m := by
      funext m; exact (h1 m).2
    rw [this]
    simpa using tendsto_const_nhds.sub hr

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 72–76 at 60a537454ac8 ↗

    1. hpart.this have (fun (m : ℕ) => ∑ a ∈ Finset.range m, f a) = fun (m : ℕ) => (1 / 2 : ℝ) - r m

      Leaves Filter.Tendsto (fun (m : ℕ) => ∑ a ∈ Finset.range m, f a) Filter.atTop (nhds (1 / 2 : ℝ)), with this : (fun (m : ℕ) => ∑ a ∈ Finset.range m, f a) = fun (m : ℕ) => (1 / 2 : ℝ) - r m.

      Uses library Finset.range range n is the set of natural numbers less than n. .

      Lean, lines 73–74
          have : (fun m => ∑ a ∈ Finset.range m, f a) = fun m => 1 / 2 - r m := by
      funext m; exact (h1 m).2

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 73–74 at 60a537454ac8 ↗

  11. hsum have HasSum f (1 / 2 : ℝ)

    Leaves ∃ (A : Set ℕ), A.Infinite ∧ ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with hsum : HasSum f (1 / 2 : ℝ).

    Uses library HasSum HasSum f a L means that the (potentially infinite) sum of the f b for b : β converges to a along the SummationFilter L. , hasSum_iff_tendsto_nat_of_nonneg A series of non-negative real numbers converges to r in the sense of HasSum if and only if the sequence of partial sum converges to r. .

    Lean, line 77
      have hsum : HasSum f (1 / 2) := (hasSum_iff_tendsto_nat_of_nonneg hfnn _).mpr hpart

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 77 at 60a537454ac8 ↗

  12. s12 case

    Leaves {a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a}.Infinite.

    Uses library sub_zero, Finset.range range n is the set of natural numbers less than n. , Finset.sum_filter.

    Lean, lines 79–100
      · -- Infinite: if A were finite the walk would be constant from some M on, so r M = 0 by hr,
    -- and 1/2 would be the finite sum of the terms taken below M, against h2.
    intro hfin
    obtain ⟨M, hM⟩ := hfin.bddAbove
    have hconst : ∀ a, M + 1 ≤ a → r a = r (M + 1) := by
      intro a ha
      induction a, ha using Nat.le_induction with
      | base => rfl
      | succ a ha ih =>
        rw [hrs a, if_neg, ih]
        intro hle
        exact absurd (hM hle) (by omega)
    have hc : Filter.Tendsto r Filter.atTop (nhds (r (M + 1))) := by
      refine tendsto_const_nhds.congr' ?_
      filter_upwards [Filter.eventually_ge_atTop (M + 1)] with a ha
      exact (hconst a ha).symm
    have hzero : r (M + 1) = 0 := tendsto_nhds_unique hc hr
    have hhalf := (h1 (M + 1)).2
    rw [hzero, sub_zero] at hhalf
    apply h2 ((Finset.range (M + 1)).filter fun a => (1 : ℝ) / (2 ^ a - 1) ≤ r a)
    rw [Finset.sum_filter]
    exact hhalf

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 79–100 at 60a537454ac8 ↗

    1. s12.s1 obtain BddAbove {a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a}

      Leaves False, with M : ℕ, hM : M ∈ upperBounds {a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a}.

      Lean, line 82
          obtain ⟨M, hM⟩ := hfin.bddAbove

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 82 at 60a537454ac8 ↗

    2. s12.hconst have ∀ (a : ℕ), M + (1 : ℕ) ≤ a → r a = r (M + (1 : ℕ))

      Leaves False, with hconst : ∀ (a : ℕ), M + (1 : ℕ) ≤ a → r a = r (M + (1 : ℕ)).

      Uses library Nat.le_induction Induction principle starting at a non-zero number. .

      Lean, lines 83–90
          have hconst : ∀ a, M + 1 ≤ a → r a = r (M + 1) := by
      intro a ha
      induction a, ha using Nat.le_induction with
      | base => rfl
      | succ a ha ih =>
        rw [hrs a, if_neg, ih]
        intro hle
        exact absurd (hM hle) (by omega)

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 83–90 at 60a537454ac8 ↗

      1. s12.hconst.s1 case

        Leaves r (M + (1 : ℕ)) = r (M + (1 : ℕ)).

        Lean, line 86
              | base => rfl

        targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 86 at 60a537454ac8 ↗

      2. s12.hconst.s2 case

        Leaves r (a + (1 : ℕ)) = r (M + (1 : ℕ)), with a : ℕ, ha : M + (1 : ℕ) ≤ a, ih : r a = r (M + (1 : ℕ)).

        Uses library Nat.succ The successor of a natural number n. , if_neg, absurd Anything follows from two contradictory hypotheses. .

        Lean, lines 87–90
              | succ a ha ih =>
        rw [hrs a, if_neg, ih]
        intro hle
        exact absurd (hM hle) (by omega)

        targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 87–90 at 60a537454ac8 ↗

    3. s12.hc have Filter.Tendsto r Filter.atTop (nhds (r (M + (1 : ℕ))))

      Leaves False, with hc : Filter.Tendsto r Filter.atTop (nhds (r (M + (1 : ℕ)))).

      Uses library Filter.Tendsto Filter.Tendsto is the generic "limit of a function" predicate. , Filter.atTop atTop is the filter representing the limit → ∞ on an ordered set. , nhds A set is called a neighborhood of x if it contains an open set around x. , tendsto_const_nhds, Filter.eventually_ge_atTop.

      Lean, lines 91–94
          have hc : Filter.Tendsto r Filter.atTop (nhds (r (M + 1))) := by
      refine tendsto_const_nhds.congr' ?_
      filter_upwards [Filter.eventually_ge_atTop (M + 1)] with a ha
      exact (hconst a ha).symm

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 91–94 at 60a537454ac8 ↗

    4. s12.hzero have r (M + (1 : ℕ)) = (0 : ℝ)

      Leaves False, with hzero : r (M + (1 : ℕ)) = (0 : ℝ).

      Uses library tendsto_nhds_unique.

      Lean, line 95
          have hzero : r (M + 1) = 0 := tendsto_nhds_unique hc hr

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 95 at 60a537454ac8 ↗

    5. s12.hhalf have (Finset.range (M + (1 : ℕ))).sum f = (1 / 2 : ℝ) - r (M + (1 : ℕ))

      Leaves False, with hhalf : (Finset.range (M + (1 : ℕ))).sum f = (1 / 2 : ℝ) - r (M + (1 : ℕ)).

      Lean, line 96
          have hhalf := (h1 (M + 1)).2

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, line 96 at 60a537454ac8 ↗

  13. s13 case

    Leaves ∑' (n : (↑{a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a} : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ).

    Uses library tsum_subtype.

    Lean, lines 101–107
      · -- The sum over A is the sum of f.
    have hind : (Set.indicator {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) = f := by
      funext a
      simp only [Set.indicator_apply, Set.mem_setOf_eq, hf]
    refine (tsum_subtype {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)).trans ?_
    rw [hind]
    exact hsum.tsum_eq

    targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 101–107 at 60a537454ac8 ↗

    1. s13.hind have ({a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a}.indicator fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) = f

      Leaves ∑' (n : (↑{a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a} : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (1 / 2 : ℝ), with hind : ({a : ℕ | (1 : ℝ) / ((2 : ℝ) ^ a - (1 : ℝ)) ≤ r a}.indicator fun (n : ℕ) => (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ))) = f.

      Uses library Set.indicator Set.indicator s f a is f a if a ∈ s, 0 otherwise. , Set.indicator_apply, Set.mem_setOf_eq Alias of Set.mem_ofPred_eq. .

      Lean, lines 102–104
          have hind : (Set.indicator {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) = f := by
      funext a
      simp only [Set.indicator_apply, Set.mem_setOf_eq, hf]

      targets/erdos-257/nodes/spec-a70fcca4/attempts/20261020T203100Z-fable-1020-e257-b-partial.lean, lines 102–104 at 60a537454ac8 ↗

import Mathlib
import Nodes.«spec-a70fcca4».Context

/-- The natural counterexample candidate for Erdős 257, stated so that it can be proved or
refuted: `1/2` is the Mersenne reciprocal sum of some infinite set. A finite set cannot give
`1/2` (finite sums have odd denominators), so any representation of `1/2` is infinite, and a
proof of this statement refutes the root. The greedy walk for `1/2` (the only possible
representation) begins 2, 3, 6, 7, 14, 20, 21, 26, 27, 32, ... and has been run without stalling
to depth 2500 here and to depth 10^8 by Hong (Zenodo 23287959, 2026, unrefereed); Kovač
(erdosproblems.com/257, Aug 2025) expects the subset-sum set, a fat Cantor set, to contain
such rationals. No proof in either direction is known. -/
theorem Opn.erdos_257_half_is_a_subsum :
    ∃ A : Set ℕ, A.Infinite ∧ ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = 1 / 2 := by
  -- approach: the greedy walk for 1/2 (take 1/(2^m-1) whenever it fits under the remainder r m); the bookkeeping is three provable holes and the open mathematics is one hole, that the walk never stalls
  -- licence: CC-BY-4.0
  -- The greedy remainder r : ℕ → ℝ has r 0 = 1/2, and position m is taken iff its term fits
  -- under r m. (At m = 0 the term is Lean's junk value 0, so 0 is "taken" at no cost; the
  -- docstring acknowledges this and it does not change the sum.) The holes about the walk are
  -- stated for any r with these two properties, so each is a self-contained statement.
  -- label: greedy remainder bookkeeping
  -- claim: $0 \le r_m$ and $\sum_{a<m,\ a\in A} \frac{1}{2^a-1} = \frac12 - r_m$ for every $m$, where $A=\{a : \frac{1}{2^a-1}\le r_a\}$
  -- The remainder never goes negative (a term is subtracted only when it fits) and is exactly
  -- 1/2 minus the sum of the terms taken so far. Induction on m.
  have h1 : ∀ r : ℕ → ℝ, r 0 = 1 / 2 →
      (∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) →
      ∀ m, 0 ≤ r m ∧
        ∑ a ∈ Finset.range m, (if (1 : ℝ) / (2 ^ a - 1) ≤ r a then (1 : ℝ) / (2 ^ a - 1) else 0)
          = 1 / 2 - r m := sorry
  -- label: no finite subsum is one half
  -- claim: $\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.
  have h2 : ∀ S : Finset ℕ, ∑ a ∈ S, (1 : ℝ) / (2 ^ a - 1) ≠ 1 / 2 := sorry
  -- label: the Mersenne reciprocal series converges
  -- claim: $\sum_{n\ge 0} \frac{1}{2^n-1} < \infty$
  -- (summable; the n = 0 term is Lean's 0.)
  -- Comparison with the geometric series: 1/(2^n-1) ≤ 2/2^n for n ≥ 1.
  have h3 : Summable (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) := sorry
  -- label: the greedy walk for one half never stalls
  -- claim: $r_m \le \sum_{k\ge 0} \frac{1}{2^{k+m}-1}$ for every $m$, for the greedy remainder $r$ of $\frac12$
  -- The open mathematics. The remainder before position m never exceeds the whole tail of the
  -- series from m on, so the walk can always continue; equivalently (given the holes above) the
  -- remainder tends to 0. Verified numerically to depth 10^8 (Hong 2026), no proof known. A
  -- stall at m would be r m > tail m, after which 1/2 is not a subset sum at all.
  have h4 : ∀ r : ℕ → ℝ, r 0 = 1 / 2 →
      (∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m) →
      ∀ m, r m ≤ ∑' k : ℕ, (1 : ℝ) / (2 ^ (k + m) - 1) := sorry
  -- The walk itself, by recursion on m.
  have hex : ∃ r : ℕ → ℝ, r 0 = 1 / 2 ∧
      ∀ m, r (m + 1) = if (1 : ℝ) / (2 ^ m - 1) ≤ r m then r m - 1 / (2 ^ m - 1) else r m :=
    ⟨fun m => Nat.rec (1 / 2 : ℝ)
        (fun k rk => if (1 : ℝ) / (2 ^ k - 1) ≤ rk then rk - 1 / (2 ^ k - 1) else rk) m,
      rfl, fun _ => rfl⟩
  obtain ⟨r, hr0, hrs⟩ := hex
  replace h1 := h1 r hr0 hrs
  replace h4 := h4 r hr0 hrs
  -- The assembly. Tail of a convergent series tends to 0, so r m → 0 by the squeeze.
  have htail : Filter.Tendsto (fun m : ℕ => ∑' k : ℕ, (1 : ℝ) / (2 ^ (k + m) - 1))
      Filter.atTop (nhds 0) := tendsto_sum_nat_add (fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))
  have hr : Filter.Tendsto r Filter.atTop (nhds 0) :=
    tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds htail (fun m => (h1 m).1) h4
  -- The partial sums of the chosen terms tend to 1/2.
  set f : ℕ → ℝ := fun a => if (1 : ℝ) / (2 ^ a - 1) ≤ r a then (1 : ℝ) / (2 ^ a - 1) else 0
    with hf
  have hfnn : ∀ a, 0 ≤ f a := by
    intro a
    simp only [hf]
    split_ifs with h
    · have h2a : (1 : ℝ) ≤ 2 ^ a := one_le_pow₀ (by norm_num)
      exact div_nonneg zero_le_one (by linarith)
    · exact le_refl 0
  have hpart : Filter.Tendsto (fun m => ∑ a ∈ Finset.range m, f a) Filter.atTop (nhds (1 / 2)) := by
    have : (fun m => ∑ a ∈ Finset.range m, f a) = fun m => 1 / 2 - r m := by
      funext m; exact (h1 m).2
    rw [this]
    simpa using tendsto_const_nhds.sub hr
  have hsum : HasSum f (1 / 2) := (hasSum_iff_tendsto_nat_of_nonneg hfnn _).mpr hpart
  refine ⟨{a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a}, ?_, ?_⟩
  · -- Infinite: if A were finite the walk would be constant from some M on, so r M = 0 by hr,
    -- and 1/2 would be the finite sum of the terms taken below M, against h2.
    intro hfin
    obtain ⟨M, hM⟩ := hfin.bddAbove
    have hconst : ∀ a, M + 1 ≤ a → r a = r (M + 1) := by
      intro a ha
      induction a, ha using Nat.le_induction with
      | base => rfl
      | succ a ha ih =>
        rw [hrs a, if_neg, ih]
        intro hle
        exact absurd (hM hle) (by omega)
    have hc : Filter.Tendsto r Filter.atTop (nhds (r (M + 1))) := by
      refine tendsto_const_nhds.congr' ?_
      filter_upwards [Filter.eventually_ge_atTop (M + 1)] with a ha
      exact (hconst a ha).symm
    have hzero : r (M + 1) = 0 := tendsto_nhds_unique hc hr
    have hhalf := (h1 (M + 1)).2
    rw [hzero, sub_zero] at hhalf
    apply h2 ((Finset.range (M + 1)).filter fun a => (1 : ℝ) / (2 ^ a - 1) ≤ r a)
    rw [Finset.sum_filter]
    exact hhalf
  · -- The sum over A is the sum of f.
    have hind : (Set.indicator {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)) = f := by
      funext a
      simp only [Set.indicator_apply, Set.mem_setOf_eq, hf]
    refine (tsum_subtype {a : ℕ | (1 : ℝ) / (2 ^ a - 1) ≤ r a} fun n : ℕ => (1 : ℝ) / (2 ^ n - 1)).trans ?_
    rw [hind]
    exact hsum.tsum_eq
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; at n = 0 the term is Lean's junk value 0, so a set containing 0 has the same sum as the set without it; the statement is unaffected and the informal problem never uses n = 0 (same reading as the root's acknowledgement).

How to read this page

How to read a statement’s page →