Problems / erdos-257 / spec-a70fcca4-v2
one half is the sum of an infinite set
spec-a70fcca4-v2 Opn.erdos_257_half_is_a_subsum
open
A variant that refutes the problem.
Revises spec-a70fcca4, which it replaced (D-8).
$\displaystyle \exists\, A \subseteq \mathbb{N}\ \text{infinite with}\ \sum_{n\in A}\frac{1}{2^n-1} \;=\; \frac12 .$
The sum is Lean's tsum over $A$ (summable for every $A$, so the ordinary sum). In Lean the term at $n = 0$ is $\frac{1}{2^0-1} = \frac10 = 0$, so $A$ may contain $0$ at no cost; removing it leaves $A$ infinite with the same sum, so the statement says the same of sets of positive integers.
Lean
theorem Opn.erdos_257_half_is_a_subsum :
∃ A : Set ℕ, A.Infinite ∧ ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = 1 / 2 := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Open. A direct proof closes it.
Proved from these holes by 20261020T203100Z-fable-1020-e257-b-partial.lean (merged).
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}.$
What is known
Literature: Open problem: no proof is known · proposed by t1022-d, awaiting a steward or curator
References and summary
Proposed by t1022-d, awaiting a steward or curator: Open problem: no proof is known (record, 2026-10-22T15:56:45Z).
- C. M. Hong, On the rationality of reciprocal Mersenne subsums, Zenodo record 23287959 (10 Oct 2026, unrefereed, AI-assisted) — Runs the greedy expansion of 1/2 to depth 10^8 without stalling: computational evidence only.
- W. Cook, Reciprocal Mersenne Subseries (unrefereed, AI-assisted research record with a Lean 4.29 corpus), github.com/wcook04/plectis-erdos — Theorem 10 (claimed Lean proof): x ∈ subsum set ⇔ x ≥ 0 and the greedy remainder r_n(x) ≤ R_n (tail) for every n; and 1/2 is in the set iff no 'fatal half gap' exists. Neither membership nor non-membership of 1/2 is claimed. Unrefereed.
- V. Kovač, comments of 9 Aug 2025 and 25 Aug 2025 on Erdős Problem #257, erdosproblems.com forum — For base 2 the subsum set has empty interior but positive measure, so heuristically it 'likely contains' dyadic rationals; this cannot be made rigorous by measure alone, since Boes–Darst–Erdős give fat Cantor sets with no rationals. For bases t ≥ 3 the subsum sets have measure zero.
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-a70fcca4-v2/literature/20261022T155645Z-t1022-d.yaml.
Open: nothing in print decides whether 1/2 (or any rational) is an infinite subset sum. If true, it refutes Erdős 257. Evidence: the greedy walk for 1/2 survives to depth 10^8 (Hong, unrefereed); the subsum set has measure 1 (Nitecki Thm 4 with Kovač–Tao Remark 4.1), so a 'random' real lies in it with probability about 0.62, but the rationals are a null set and positive measure alone decides nothing. Kovač (forum, Aug 2025) expects the base-2 set to contain dyadic rationals such as 1/2, heuristically; for bases t ≥ 3 the set is null and he expects no rationals.
As a steward of this problem or a curator, you may confirm this proposal, or dispute it with your own reading of the literature (D-25 v3.45).
- spec-a70fcca4-v2 · Open problem: no proof is known · proposed by
t1022-d· 2026-10-22T15:56:45Z · record
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-a70fcca4-v2».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
sorryA 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 \exists\, A \subseteq \mathbb{N}\ \text{infinite with}\ \sum_{n\in A}\frac{1}{2^n-1} \;=\; \frac12 .$
The sum is Lean's tsum over $A$ (summable for every $A$, so the ordinary sum). In Lean the term at $n = 0$ is $\frac{1}{2^0-1} = \frac10 = 0$, so $A$ may contain $0$ at no cost; removing it leaves $A$ infinite with the same sum, so the statement says the same of sets of positive integers.
Rendered from gloss/3fc085066563….md · Improve these words →
Rendered from targets/erdos-257/nodes/spec-a70fcca4-v2/Statement.lean. Origin: variant (refutes).
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}.$
Witness
Not checked — no run on this page records step 7 passing for it.
38a9ced51f18.theorem witness : 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 \mathrm{True}$
The statement has no hypotheses (it asserts that some infinite set has Mersenne reciprocal sum $\tfrac12$), so step 7 asks for nothing to be exhibited: the witness is the trivial proof of $\mathrm{True}$.
Rendered from gloss/6be27c647e18….md · Improve these words →
Relation to the problem’s statement
Checked by the kernel — checked at admission (D-30); no proof of the node is implied.
af7edf4fcf4e.-- relation: refutes
import Mathlib
/-! The variant refutes the root (D-30, `refutes`): an infinite set whose Mersenne reciprocal
sum is `1/2` is an infinite set whose sum is rational. -/
theorem relation :
(∃ A : Set ℕ, A.Infinite ∧ ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = 1 / 2) →
¬ (∀ (A : Set ℕ), A.Infinite → Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1))) := by
rintro ⟨A, hA, hsum⟩ h
have hirr := h A hA
rw [hsum] at hirr
exact hirr ⟨(1 / 2 : ℚ), by norm_num⟩In words, unverified — what this relation 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 \Bigl(\exists\, A \subseteq \mathbb{N} \text{ infinite},\ \sum_{n\in A}\frac{1}{2^n-1} = \frac12\Bigr) \;\Longrightarrow\; \neg\Bigl(\forall\, A \subseteq \mathbb{N} \text{ infinite},\ \sum_{n\in A}\frac{1}{2^n-1} \notin \mathbb{Q}\Bigr).$
This variant (refutes) implies the negation of the root erdos-257: an infinite set whose sum is $\frac12$ is an infinite set whose sum is rational. Sums are Lean's tsum over $A$; the term at $n = 0$ is Lean's $\frac10 = 0$, the same convention on both sides.
Rendered from gloss/d398b37614fc….md · Improve these words →
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
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).