Problems / erdos-257 / variant-5c939e77
only countably many sets have a rational sum
variant-5c939e77
proved
A related variant. not yet signed as pertinent to the target (D-30 v3.12)
$\displaystyle \Bigl\{\, A \subseteq \mathbb{N} \ :\ 0 \notin A,\ \ \sum_{n\in A}\frac{1}{2^n-1} \in \mathbb{Q} \,\Bigr\} \ \text{ is countable}.$
Finite and infinite $A$ alike: the family of sets of positive integers whose sum is rational is countable. Sums are Lean's tsum over the set, the ordinary sum of a convergent nonnegative series; the term at $n = 0$ is Lean's $\frac{1}{2^0-1} = \frac10 = 0$.
Lean
theorem Opn.erdos_257_rational_subsums_countable :
{A : Set ℕ | 0 ∉ A ∧ ∃ q : ℚ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = q}.Countable := 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 was proved
Proved by Proof.lean, checked by the kernel. Its attestation, 000853, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000853.json, merge commit d8cea3cddcb4.
Outline of Proof.lean, extracted by the gate at 1bd7ca70c9ee from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.
s1caseLeaves
Set.MapsTo (fun (A : Set ℕ) => ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))) {A : Set ℕ | (0 : ℕ) ∉ A ∧ ∃ (q : ℚ), ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑q : ℝ)} (Set.range Rat.cast).Uses library
Exists.introExistential introduction. .Lean, lines 16–17
· rintro A ⟨_, q, hq⟩ exact ⟨q, hq.symm⟩targets/erdos-257/nodes/variant-5c939e77/Proof.lean, lines 16–17 at
d8cea3cddcb4↗s2caseLeaves
Set.InjOn (fun (A : Set ℕ) => ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ))) {A : Set ℕ | (0 : ℕ) ∉ A ∧ ∃ (q : ℚ), ∑' (n : (↑A : Type)), (1 : ℝ) / ((2 : ℝ) ^ (↑n : ℕ) - (1 : ℝ)) = (↑q : ℝ)}.Uses statements spec-5e2e0890
Opn.erdos_257_subsum_injective.Lean, lines 18–19
· rintro A ⟨hA, _⟩ B ⟨hB, _⟩ h exact Opn.erdos_257_subsum_injective A B hA hB htargets/erdos-257/nodes/variant-5c939e77/Proof.lean, lines 18–19 at
d8cea3cddcb4↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000853.json, merge commit d8cea3cddcb4.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/variant-5c939e77/Proof.lean, sha256 08fd3976ed71.import Mathlib
import Nodes.«variant-5c939e77».Context
/-- Only countably many sets of positive integers have a rational Mersenne reciprocal sum, so
Erdős 257 has at most countably many counterexamples. This is the "immediate consequence" that
Kovač and Tao draw from the distinctness of the subset sums (V. Kovač and T. Tao, *On several
irrationality problems for Ahmes series*, arXiv:2406.17593 v4, §2.1.2 p. 4 and Remark 4.1
p. 13; Acta Math. Hungar. 175 (2025)). Finite sets are included: every finite set has a
rational sum, and the statement says the whole family is still countable. It follows from
uniqueness of representation (`spec-5e2e0890`) because the rationals are countable. -/
theorem Opn.erdos_257_rational_subsums_countable :
{A : Set ℕ | 0 ∉ A ∧ ∃ q : ℚ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = q}.Countable := by
refine Set.MapsTo.countable_of_injOn
(f := fun A : Set ℕ => ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1))
(t := Set.range ((↑) : ℚ → ℝ)) ?_ ?_ (Set.countable_range _)
· rintro A ⟨_, q, hq⟩
exact ⟨q, hq.symm⟩
· rintro A ⟨hA, _⟩ B ⟨hB, _⟩ h
exact Opn.erdos_257_subsum_injective A B hA hB hWhat is known
Literature: Elementary: a routine formalisation of a known fact · proposed by t1022-d, awaiting a steward or curator
References and summary
Proposed by t1022-d, awaiting a steward or curator: Elementary: a routine formalisation of a known fact (record, 2026-10-22T15:22:15Z).
- V. Kovač and T. Tao, On several irrationality problems for Ahmes series, arXiv:2406.17593v4; Acta Math. Hungar. 175 (2025), 572–608 — §2.1.2 p. 4: the subsums for distinct A are distinct and form a Cantor set; 'Its immediate consequence is that there can be only at most countably many counterexamples'. Remark 4.1 p. 13 proves the distinctness.
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1022-d, drafted with Claude Opus 5.5 (Claude Code); papers read 2026-10-22 from the linked PDFs. Rendered from targets/erdos-257/nodes/variant-5c939e77/literature/20261022T152215Z-t1022-d.yaml.
Elementary: distinct sets have distinct sums (spec-5e2e0890 on this graph), and there are countably many 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).
- variant-5c939e77 · Elementary: a routine formalisation of a known fact · proposed by
t1022-d· 2026-10-22T15:22:15Z · record
Work on it
No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).
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.«variant-5c939e77».Context
/-- Only countably many sets of positive integers have a rational Mersenne reciprocal sum, so
Erdős 257 has at most countably many counterexamples. This is the "immediate consequence" that
Kovač and Tao draw from the distinctness of the subset sums (V. Kovač and T. Tao, *On several
irrationality problems for Ahmes series*, arXiv:2406.17593 v4, §2.1.2 p. 4 and Remark 4.1
p. 13; Acta Math. Hungar. 175 (2025)). Finite sets are included: every finite set has a
rational sum, and the statement says the whole family is still countable. It follows from
uniqueness of representation (`spec-5e2e0890`) because the rationals are countable. -/
theorem Opn.erdos_257_rational_subsums_countable :
{A : Set ℕ | 0 ∉ A ∧ ∃ q : ℚ, ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = q}.Countable := 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 \Bigl\{\, A \subseteq \mathbb{N} \ :\ 0 \notin A,\ \ \sum_{n\in A}\frac{1}{2^n-1} \in \mathbb{Q} \,\Bigr\} \ \text{ is countable}.$
Finite and infinite $A$ alike: the family of sets of positive integers whose sum is rational is countable. Sums are Lean's tsum over the set, the ordinary sum of a convergent nonnegative series; the term at $n = 0$ is Lean's $\frac{1}{2^0-1} = \frac10 = 0$.
Rendered from gloss/0ecf7cd1affd….md · Improve these words →
Rendered from targets/erdos-257/nodes/variant-5c939e77/Statement.lean. Origin: variant (related).
Depends on (1), each in words
Depends on, each in words where someone has written them:
- spec-5e2e0890
Opn.erdos_257_subsum_injective: $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 .$ · used by the proof
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000853.json, merge commit d8cea3cddcb4.
Verdict pass, from attestations/000853.json.
- Submitter
t1022-d- Toolchain
- leanprover/lean4:v4.33.1 (hash
f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63) - Mathlib
- 0df444a360eaa60ab8c11dca51a86af692955474
- Reviewer
- none needed (intermediate)
| Step | Check | Result |
|---|---|---|
| 1 | toolchain | pass |
| 2 | paths | pass |
| 4 | kernel-replay | pass |
| 5 | axioms | pass |
| 6 | hazards | pass |
| 7 | witness | pass |
| 8 | deps | pass |
Witness
Checked by the kernel — step 7 passed in the run its attestation records: attestations/000853.json, merge commit d8cea3cddcb4.
fc9e04aa384d.import Nodes.«variant-5c939e77».Context theorem witness : True := trivial
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
Acknowledged findings (1)
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a div-zero finding at 1 / (2 ^ ↑n - 1)
Real division; the sets in question exclude 0 by hypothesis, so every divisor 2^n - 1 is positive.