Problems / erdos-257 / variant-2f5236aa
the case A = all naturals (Erdős 1948)
variant-2f5236aa
proved
Restated as hole h_naturals of erdos-257 (split by 20261023T133841Z-t1023-f1-partial.lean).
$\displaystyle \sum_{n=0}^{\infty}\frac{1}{2^n-1} \ \text{ is irrational}.$
The case $A = \mathbb{N}$ of the root. In Lean the term at $n = 0$ is $\frac{1}{2^0-1} = \frac10 = 0$, so the sum is $\sum_{n\ge1}\frac{1}{2^n-1}$; the series converges, and Lean's tsum is its ordinary sum.
Lean
theorem Opn.erdos_257_all_naturals :
Irrational (∑' n : ℕ, (1 : ℝ) / (2 ^ n - 1)) := 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 →
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/5186eb0814cf….md, written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22.
Overview
Draft · drafted, by the model named above
Write $d(n)$ for the number of divisors of $n$ (with $d(0) = 0$). The proof is Erdős's 1948 argument: the series is rewritten as $\sum_n d(n)/2^n$, a rational value would make every scaled tail of that series a positive integer, the Chinese remainder theorem makes $m$ consecutive divisor counts divisible by $2^m$, which forces such a tail to be at least $2^m$, and averaging along an arithmetic progression shows the tails are on average far smaller. All the work is in private helper declarations; the theorem itself rewrites with series_eq and applies irrational_dd_series.
The Lambert series. series_eq: $\sum_{n \ge 0} \frac{1}{2^n - 1} = \sum_{n \ge 0} \frac{d(n)}{2^n}$. This is Mathlib's tsum_pow_div_one_sub_eq_tsum_sigma at $r = \frac12$ and $k = 0$, after moving between sums over $\mathbb{N}$ and over the positive integers (both $n = 0$ terms are $0$ in Lean).
Tails are integers. Suppose $\sum_n d(n)/2^n = a/b$ with $a \in \mathbb{Z}$ and $b \ge 1$ (the numerator and denominator of the rational). For each $j$ let $T_j = b \sum_{i \ge 1} d(j+i)/2^i$. Splitting the series after $n = j$ and multiplying by $2^j$ gives (tail_eq_Zint) $$T_j = 2^j a - b \sum_{n=0}^{j} d(n)\, 2^{\,j-n} \in \mathbb{Z},$$ and $T_j > 0$ because $d(j+1) \ge 1$ (tail_pos).
Forced divisibility. pow_two_dvd_dd: if $m$ distinct primes each divide $n \ne 0$ exactly once, then $2^m \mid d(n)$, since $d(n) = \prod_{p \mid n} (v_p(n) + 1)$ and each of those $m$ factors is $2$. Zint_dvd: if $2^m \mid d(n)$ for every $n$ with $k < n \le k+m$, then $2^m \mid T_{k+m}$, because in the formula above every term with $n \le k$ carries the factor $2^{k+m-n} \ge 2^m$. So in that case $T_{k+m} \ge 2^m$.
Choosing the primes. Take $m \ge b$ with $15 m^5 < 2^m$ (exists_param) and $q = 2(m + m^2)m^2$. Bertrand's postulate gives a prime $P_e \in (2^e, 2^{e+1}]$ for each $e$, increasing in $e$. The $m^2$ primes $p_{ij} = P_{m + im + j}$, $0 \le i, j < m$, are distinct, exceed $2^m$, and their squares multiply to $Q = \prod p_{ij}^2 \le 2^q$. The Chinese remainder theorem gives $c < Q$ with $c + i + 1 \equiv p_{ij} \pmod{p_{ij}^2}$ for all $i, j$. Hence for every $t$ and every $i < m$, the number $c + tQ + i + 1$ is divisible by each of $p_{i0}, \dots, p_{i,m-1}$ exactly once, so $2^m \mid d(n)$ for $c + tQ < n \le c + tQ + m$, and therefore $$T_{c+tQ+m} \ge 2^m \quad \text{for every } t \ge 0.$$ Since every $p_{ij}$ exceeds $m + 3q$, the numbers $c + m + i + 1$ with $i < 3q$ are coprime to $Q$.
The averaging contradiction. averaging_contra. Put $L = 3q$ and $X = Q + m + L$. Bounding $d(n) \le n$ beyond the first $L$ terms (tail_upper) gives $$T_j \le b \sum_{i < L} \frac{d(j+i+1)}{2^{i+1}} + b\,\frac{j+L+2}{2^L}.$$ For $r$ coprime to $Q$ and $r + tQ \le X^2$ when $t < X$, sum_dd_AP_le bounds $\sum_{t<X} d(r + tQ) \le 2X(2 + \log X)$: each divisor pairs with one at most the square root (dd_le_two_mul_small), and at most $X/e + 1$ of the $t < X$ have $e \mid r + tQ$ (card_AP_dvd_le). Summing the lower bound over $t < X$ and using these estimates yields $X\, 2^m \le b \cdot 2X(2 + \log X) + X$, that is $2^m \le 2b(2 + \log X) + 1$. As $X \le 2^{q+1}$, $\log X \le q + 1$, so $2^m \le 2b(3+q) + 1$, which the choice of $m$ makes false (param_facts).
Read it step by step (1 more section)
The assembly
Draft · drafted, by the model named above
The theorem rewrites the sum with series_eq as $\sum_n d(n)/2^n$ and closes with irrational_dd_series, the irrationality of that series proved above.
History: 1 version on record
2026-10-22 · written by t1022-k, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · current · explainer/5186eb0814cf….md · the first version of its chain
Read this version
Overview
Write $d(n)$ for the number of divisors of $n$ (with $d(0) = 0$). The proof is Erdős's 1948 argument: the series is rewritten as $\sum_n d(n)/2^n$, a rational value would make every scaled tail of that series a positive integer, the Chinese remainder theorem makes $m$ consecutive divisor counts divisible by $2^m$, which forces such a tail to be at least $2^m$, and averaging along an arithmetic progression shows the tails are on average far smaller. All the work is in private helper declarations; the theorem itself rewrites with
series_eqand appliesirrational_dd_series.The Lambert series.
series_eq: $\sum_{n \ge 0} \frac{1}{2^n - 1} = \sum_{n \ge 0} \frac{d(n)}{2^n}$. This is Mathlib'stsum_pow_div_one_sub_eq_tsum_sigmaat $r = \frac12$ and $k = 0$, after moving between sums over $\mathbb{N}$ and over the positive integers (both $n = 0$ terms are $0$ in Lean).Tails are integers. Suppose $\sum_n d(n)/2^n = a/b$ with $a \in \mathbb{Z}$ and $b \ge 1$ (the numerator and denominator of the rational). For each $j$ let $T_j = b \sum_{i \ge 1} d(j+i)/2^i$. Splitting the series after $n = j$ and multiplying by $2^j$ gives (
tail_eq_Zint) $$T_j = 2^j a - b \sum_{n=0}^{j} d(n)\, 2^{\,j-n} \in \mathbb{Z},$$ and $T_j > 0$ because $d(j+1) \ge 1$ (tail_pos).Forced divisibility.
pow_two_dvd_dd: if $m$ distinct primes each divide $n \ne 0$ exactly once, then $2^m \mid d(n)$, since $d(n) = \prod_{p \mid n} (v_p(n) + 1)$ and each of those $m$ factors is $2$.Zint_dvd: if $2^m \mid d(n)$ for every $n$ with $k < n \le k+m$, then $2^m \mid T_{k+m}$, because in the formula above every term with $n \le k$ carries the factor $2^{k+m-n} \ge 2^m$. So in that case $T_{k+m} \ge 2^m$.Choosing the primes. Take $m \ge b$ with $15 m^5 < 2^m$ (
exists_param) and $q = 2(m + m^2)m^2$. Bertrand's postulate gives a prime $P_e \in (2^e, 2^{e+1}]$ for each $e$, increasing in $e$. The $m^2$ primes $p_{ij} = P_{m + im + j}$, $0 \le i, j < m$, are distinct, exceed $2^m$, and their squares multiply to $Q = \prod p_{ij}^2 \le 2^q$. The Chinese remainder theorem gives $c < Q$ with $c + i + 1 \equiv p_{ij} \pmod{p_{ij}^2}$ for all $i, j$. Hence for every $t$ and every $i < m$, the number $c + tQ + i + 1$ is divisible by each of $p_{i0}, \dots, p_{i,m-1}$ exactly once, so $2^m \mid d(n)$ for $c + tQ < n \le c + tQ + m$, and therefore $$T_{c+tQ+m} \ge 2^m \quad \text{for every } t \ge 0.$$ Since every $p_{ij}$ exceeds $m + 3q$, the numbers $c + m + i + 1$ with $i < 3q$ are coprime to $Q$.The averaging contradiction.
averaging_contra. Put $L = 3q$ and $X = Q + m + L$. Bounding $d(n) \le n$ beyond the first $L$ terms (tail_upper) gives $$T_j \le b \sum_{i < L} \frac{d(j+i+1)}{2^{i+1}} + b\,\frac{j+L+2}{2^L}.$$ For $r$ coprime to $Q$ and $r + tQ \le X^2$ when $t < X$,sum_dd_AP_lebounds $\sum_{t<X} d(r + tQ) \le 2X(2 + \log X)$: each divisor pairs with one at most the square root (dd_le_two_mul_small), and at most $X/e + 1$ of the $t < X$ have $e \mid r + tQ$ (card_AP_dvd_le). Summing the lower bound over $t < X$ and using these estimates yields $X\, 2^m \le b \cdot 2X(2 + \log X) + X$, that is $2^m \le 2b(2 + \log X) + 1$. As $X \le 2^{q+1}$, $\log X \le q + 1$, so $2^m \le 2b(3+q) + 1$, which the choice of $m$ makes false (param_facts).The assembly (close)
The theorem rewrites the sum with
series_eqas $\sum_n d(n)/2^n$ and closes withirrational_dd_series, the irrationality of that series proved above.
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, 000846, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000846.json, merge commit 3afc7ec48bb1.
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.
closetermIrrational (∑' (n : ℕ), (1 : ℝ) / ((2 : ℝ) ^ n - (1 : ℝ)))Closes the goal.
Lean, lines 572–573
rw [series_eq] exact irrational_dd_series
targets/erdos-257/nodes/variant-2f5236aa/Proof.lean, lines 572–573 at
3afc7ec48bb1↗
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000846.json, merge commit 3afc7ec48bb1.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-257/nodes/variant-2f5236aa/Proof.lean, sha256 ad9d7b838ad7.import Mathlib
import Nodes.«variant-2f5236aa».Context
/- The divisor-counting function. -/
private def dd (n : ℕ) : ℕ := n.divisors.card
/- `b` times the "tail" `∑_{i ≥ 1} d(j+i) / 2^i`. -/
private noncomputable def Tail (b : ℕ) (j : ℕ) : ℝ := b * ∑' i : ℕ, (dd (j + i + 1) : ℝ) / 2 ^ (i + 1)
/- The integer that the tail equals when the series is `a / b`. -/
private def Zint (a : ℤ) (b : ℕ) (j : ℕ) : ℤ :=
a * 2 ^ j - b * ∑ n ∈ Finset.range (j + 1), (dd n : ℤ) * 2 ^ (j - n)
private lemma dd_le (n : ℕ) : dd n ≤ n := Nat.card_divisors_le_self n
private lemma dd_pos {n : ℕ} (hn : 0 < n) : 0 < dd n := by
unfold dd; exact Finset.card_pos.mpr ⟨1, by simp; omega⟩
private lemma summable_dd_shift (j : ℕ) : Summable (fun i : ℕ => (dd (j + i + 1) : ℝ) / 2 ^ (i + 1)) := by
have h : Summable (fun i : ℕ => ((j + 1 : ℝ) + i) * (1/2) ^ i) := by
have h1 := (summable_geometric_two).mul_left (j+1 : ℝ)
have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
(by norm_num [abs_of_pos])
simpa [add_mul] using h1.add h2
refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h
have : (dd (j + i + 1) : ℝ) ≤ j + i + 1 := by exact_mod_cast Nat.card_divisors_le_self _
rw [div_eq_mul_inv, pow_succ, mul_inv, one_div, inv_pow]
have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
nlinarith
private lemma summable_dd : Summable (fun n : ℕ => (dd n : ℝ) / 2 ^ n) := by
have h2 := summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
(by norm_num [abs_of_pos])
refine Summable.of_nonneg_of_le (fun i => by positivity) (fun i => ?_) h2
have : (dd i : ℝ) ≤ i := by exact_mod_cast Nat.card_divisors_le_self _
rw [div_eq_mul_inv, one_div, inv_pow, pow_one]
have : (0:ℝ) ≤ (2 ^ i)⁻¹ := by positivity
nlinarith
private lemma tail_pos {b : ℕ} (hb : 0 < b) (j : ℕ) : 0 < Tail b j := by
unfold Tail
apply mul_pos (by exact_mod_cast hb)
apply (summable_dd_shift j).tsum_pos (fun i => by positivity) 0
have := dd_pos (n := j + 0 + 1) (by omega)
positivity
private lemma tail_upper (b j L : ℕ) :
Tail b j ≤ b * ∑ i ∈ Finset.range L, (dd (j + i + 1) : ℝ) / 2 ^ (i + 1)
+ b * ((j + L + 2 : ℝ) / 2 ^ L) := by
unfold Tail
rw [← (summable_dd_shift j).sum_add_tsum_nat_add L, mul_add]
gcongr
have hg1 : Summable (fun i : ℕ => (1/2 : ℝ) ^ i) := summable_geometric_two
have hg2 : Summable (fun i : ℕ => (i : ℝ) * (1/2 : ℝ) ^ i) := by
simpa using summable_pow_mul_geometric_of_norm_lt_one 1 (r := (1/2 : ℝ))
(by norm_num [abs_of_pos])
have key : ∑' i : ℕ, ((j + L + 1 : ℝ) / 2 ^ (L + 1) * (1/2) ^ i
+ 1 / 2 ^ (L + 1) * ((i : ℝ) * (1/2) ^ i)) = (j + L + 2 : ℝ) / 2 ^ L := by
rw [(hg1.mul_left _).tsum_add (hg2.mul_left _), tsum_mul_left, tsum_mul_left,
tsum_geometric_two, tsum_coe_mul_geometric_of_norm_lt_one (by norm_num [abs_of_pos])]
rw [pow_succ]; field_simp; ring
rw [← key]
refine Summable.tsum_le_tsum (fun i => ?_) ((summable_nat_add_iff L).mpr (summable_dd_shift j))
((hg1.mul_left _).add (hg2.mul_left _))
have : (dd (j + (i + L) + 1) : ℝ) ≤ j + L + 1 + i := by
have := Nat.card_divisors_le_self (j + (i + L) + 1)
have : (dd (j + (i + L) + 1) : ℝ) ≤ ((j + (i + L) + 1 : ℕ) : ℝ) := by exact_mod_cast this
push_cast at this; linarith
show (dd (j + (i + L) + 1) : ℝ) / 2 ^ (i + L + 1) ≤ _
rw [show (2:ℝ) ^ (i + L + 1) = 2 ^ (L+1) * 2 ^ i by ring, one_div_pow]
rw [div_le_iff₀ (by positivity)]
field_simp
linarith
private lemma tsum_pnat_of_zero (f : ℕ → ℝ) (h0 : f 0 = 0) : ∑' n : ℕ+, f n = ∑' n : ℕ, f n := by
apply Function.Injective.tsum_eq PNat.coe_injective
intro n hn
have : n ≠ 0 := by rintro rfl; exact hn h0
exact ⟨⟨n, Nat.pos_of_ne_zero this⟩, rfl⟩
/- The Lambert series identity `∑ 1/(2^n-1) = ∑ d(n)/2^n`. -/
private lemma series_eq : ∑' n : ℕ, (1 : ℝ) / (2 ^ n - 1) = ∑' n : ℕ, (dd n : ℝ) / 2 ^ n := by
have h := tsum_pow_div_one_sub_eq_tsum_sigma (𝕜 := ℝ) (r := 1/2) (by norm_num [abs_of_pos]) 0
rw [← tsum_pnat_of_zero _ (by simp), ← tsum_pnat_of_zero _ (by simp [dd])]
convert h using 1
· apply tsum_congr; intro n
have : (2:ℝ) ^ (n:ℕ) - 1 ≠ 0 := by
have : (1:ℝ) < 2 ^ (n:ℕ) := one_lt_pow₀ (by norm_num) n.ne_zero
linarith
have h2 : (1 - (1/2:ℝ) ^ (n:ℕ)) ≠ 0 := by
have : (1/2:ℝ) ^ (n:ℕ) < 1 := pow_lt_one₀ (by norm_num) (by norm_num) n.ne_zero
linarith
rw [one_div_pow]
field_simp
· apply tsum_congr; intro n
simp [ArithmeticFunction.sigma_zero_apply, dd, div_eq_mul_inv]
private lemma tail_eq_Zint {a : ℤ} {b : ℕ} (hb : 0 < b)
(h : ∑' n : ℕ, (dd n : ℝ) / 2 ^ n = a / b) (j : ℕ) : Tail b j = Zint a b j := by
have hsplit := summable_dd.sum_add_tsum_nat_add (j + 1)
have htail : ∑' i : ℕ, (dd (i + (j + 1)) : ℝ) / 2 ^ (i + (j + 1)) =
(1 / 2 ^ j) * ∑' i : ℕ, (dd (j + i + 1) : ℝ) / 2 ^ (i + 1) := by
rw [← tsum_mul_left]
apply tsum_congr; intro i
rw [show i + (j + 1) = j + i + 1 by ring,
show (2:ℝ) ^ (j + i + 1) = 2 ^ j * 2 ^ (i + 1) by ring]
field_simp
rw [htail, h] at hsplit
have hb' : (b : ℝ) ≠ 0 := by exact_mod_cast hb.ne'
have hT : Tail b j = 2 ^ j * (a - b * ∑ n ∈ Finset.range (j + 1), (dd n : ℝ) / 2 ^ n) := by
unfold Tail
field_simp at hsplit
have : (2:ℝ) ^ j ≠ 0 := by positivity
field_simp
linear_combination hsplit
rw [hT]
unfold Zint
push_cast
rw [mul_sub, Finset.mul_sum, Finset.mul_sum, Finset.mul_sum]
congr 1
· ring
· apply Finset.sum_congr rfl; intro n hn
have hn' : n ≤ j := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
rw [pow_sub₀ _ (by norm_num) hn']
field_simp
private lemma Zint_dvd (a : ℤ) (b k m : ℕ) (hd : ∀ n, k < n → n ≤ k + m → 2 ^ m ∣ dd n) :
(2 : ℤ) ^ m ∣ Zint a b (k + m) := by
unfold Zint
apply dvd_sub
· exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
· apply Dvd.dvd.mul_left
apply Finset.dvd_sum
intro n hn
have hn' : n ≤ k + m := Nat.lt_succ_iff.mp (Finset.mem_range.mp hn)
by_cases hnk : n ≤ k
· exact Dvd.dvd.mul_left (pow_dvd_pow 2 (by omega)) _
· apply Dvd.dvd.mul_right
exact_mod_cast hd n (by omega) hn'
/- If `m` distinct primes each divide `n` exactly once, then `2^m ∣ d(n)`. -/
private lemma pow_two_dvd_dd {n : ℕ} (hn : n ≠ 0) (S : Finset ℕ)
(hS : ∀ p ∈ S, p.Prime ∧ p ∣ n ∧ ¬ p ^ 2 ∣ n) : 2 ^ S.card ∣ dd n := by
unfold dd
rw [Nat.card_divisors hn]
have hsub : S ⊆ n.primeFactors := by
intro p hp
obtain ⟨h1, h2, _⟩ := hS p hp
exact Nat.mem_primeFactors.mpr ⟨h1, h2, hn⟩
have : 2 ^ S.card = ∏ p ∈ S, (n.factorization p + 1) := by
rw [← Finset.prod_const]
apply Finset.prod_congr rfl
intro p hp
obtain ⟨h1, h2, h3⟩ := hS p hp
have e1 : 1 ≤ n.factorization p := (h1.dvd_iff_one_le_factorization hn).mp h2
have e2 : ¬ 2 ≤ n.factorization p := fun h => h3 ((h1.pow_dvd_iff_le_factorization hn).mpr h)
omega
rw [this]
exact Finset.prod_dvd_prod_of_subset _ _ _ hsub
private lemma dd_le_two_mul_small (n : ℕ) :
dd n ≤ 2 * (n.divisors.filter (fun e => e * e ≤ n)).card := by
unfold dd
rw [← Finset.card_filter_add_card_filter_not (fun e => e * e ≤ n)]
have : (n.divisors.filter (fun e => ¬ e * e ≤ n)).card ≤
(n.divisors.filter (fun e => e * e ≤ n)).card := by
apply Finset.card_le_card_of_injOn (fun e => n / e)
· intro e he
simp only [Finset.coe_filter, Nat.mem_divisors, not_le, Set.mem_setOf_eq] at he ⊢
obtain ⟨⟨hd, hn⟩, hlt⟩ := he
have hepos : 0 < e := Nat.pos_of_dvd_of_pos hd (Nat.pos_of_ne_zero hn)
refine ⟨⟨Nat.div_dvd_of_dvd hd, hn⟩, ?_⟩
have h1 : n / e < e := (Nat.div_lt_iff_lt_mul hepos).mpr hlt
calc n / e * (n / e) ≤ n / e * e := Nat.mul_le_mul_left _ h1.le
_ = n := Nat.div_mul_cancel hd
· intro e1 h1 e2 h2 h
simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
have := congrArg (fun x => n / x) h
simp only at this
rwa [Nat.div_div_self h1.1.1 h1.1.2, Nat.div_div_self h2.1.1 h2.1.2] at this
omega
private lemma card_AP_dvd_le (r Q X e : ℕ) (hcop : Nat.Coprime r Q) :
((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card ≤ X / (e + 1) + 1 := by
set E := e + 1 with hE
have hEpos : 0 < E := by omega
have key : ∀ t1 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q),
∀ t2 ∈ (Finset.range X).filter (fun t => E ∣ r + t * Q), t1 / E = t2 / E → t1 ≤ t2 → t1 = t2 := by
intro t1 h1 t2 h2 hq hle
simp only [Finset.mem_filter, Finset.mem_range] at h1 h2
have hcopE : Nat.Coprime E Q := by
have hg1 : Nat.gcd E Q ∣ r + t1 * Q := (Nat.gcd_dvd_left E Q).trans h1.2
have hg2 : Nat.gcd E Q ∣ t1 * Q := Dvd.dvd.mul_left (Nat.gcd_dvd_right E Q) _
have hg3 : Nat.gcd E Q ∣ r := (Nat.dvd_add_left hg2).mp hg1
have hg4 : Nat.gcd E Q ∣ Nat.gcd r Q := Nat.dvd_gcd hg3 (Nat.gcd_dvd_right E Q)
rw [hcop] at hg4
exact Nat.dvd_one.mp hg4
have hd : E ∣ (t2 - t1) * Q := by
have := Nat.dvd_sub h2.2 h1.2
rwa [show r + t2 * Q - (r + t1 * Q) = (t2 - t1) * Q by rw [Nat.sub_mul]; omega] at this
have hd2 : E ∣ t2 - t1 := hcopE.dvd_of_dvd_mul_right hd
have hlt : t2 - t1 < E := by
have e1 := Nat.div_add_mod t1 E
have e2 := Nat.div_add_mod t2 E
have m1 := Nat.mod_lt t1 hEpos
have m2 := Nat.mod_lt t2 hEpos
rw [hq] at e1
omega
have := Nat.eq_zero_of_dvd_of_lt hd2 hlt
omega
calc ((Finset.range X).filter (fun t => E ∣ r + t * Q)).card ≤ (Finset.range (X / E + 1)).card := by
apply Finset.card_le_card_of_injOn (fun t => t / E)
· intro t ht
simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq] at ht
simp only [Finset.coe_range, Set.mem_Iio]
have := Nat.div_le_div_right (c := E) ht.1.le
omega
· intro t1 h1 t2 h2 hq
rcases le_total t1 t2 with h | h
· exact key t1 h1 t2 h2 hq h
· exact (key t2 h2 t1 h1 hq.symm h).symm
_ = X / E + 1 := Finset.card_range _
private lemma sum_dd_AP_le (r Q X : ℕ) (hcop : Nat.Coprime r Q)
(hX : ∀ t < X, r + t * Q ≤ X * X) :
(∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤ 2 * X * (2 + Real.log X) := by
have hnat : ∑ t ∈ Finset.range X, dd (r + t * Q) ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
calc ∑ t ∈ Finset.range X, dd (r + t * Q)
≤ ∑ t ∈ Finset.range X, 2 * ((Finset.range X).filter (fun e => (e + 1) ∣ r + t * Q)).card := by
apply Finset.sum_le_sum; intro t ht
refine (dd_le_two_mul_small _).trans ?_
apply Nat.mul_le_mul_left
apply Finset.card_le_card_of_injOn (fun e => e - 1)
· intro e he
simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at he
simp only [Finset.coe_filter, Finset.mem_range, Set.mem_setOf_eq]
have hepos : 0 < e := Nat.pos_of_dvd_of_pos he.1.1 (Nat.pos_of_ne_zero he.1.2)
have : e * e ≤ X * X := he.2.trans (hX t (by simpa using ht))
have : e ≤ X := Nat.mul_self_le_mul_self_iff.mp this
refine ⟨by omega, ?_⟩
rw [Nat.sub_add_cancel hepos]; exact he.1.1
· intro e1 h1 e2 h2 h
simp only [Finset.coe_filter, Nat.mem_divisors, Set.mem_setOf_eq] at h1 h2
have := Nat.pos_of_dvd_of_pos h1.1.1 (Nat.pos_of_ne_zero h1.1.2)
have := Nat.pos_of_dvd_of_pos h2.1.1 (Nat.pos_of_ne_zero h2.1.2)
simp only at h
omega
_ = 2 * ∑ e ∈ Finset.range X, ((Finset.range X).filter (fun t => (e + 1) ∣ r + t * Q)).card := by
rw [← Finset.mul_sum]
congr 1
simp only [Finset.card_filter]
exact Finset.sum_comm
_ ≤ 2 * ∑ e ∈ Finset.range X, (X / (e + 1) + 1) := by
apply Nat.mul_le_mul_left
exact Finset.sum_le_sum fun e _ => card_AP_dvd_le r Q X e hcop
have hreal : ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) ≤ X * (1 + Real.log X) + X := by
push_cast
rw [Finset.sum_add_distrib]
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, mul_one]
gcongr
calc ∑ e ∈ Finset.range X, ((X / (e + 1) : ℕ) : ℝ) ≤ ∑ e ∈ Finset.range X, (X : ℝ) / (e + 1) := by
apply Finset.sum_le_sum; intro e _
have := Nat.cast_div_le (α := ℝ) (m := X) (n := e + 1)
push_cast at this; exact this
_ = X * (harmonic X : ℝ) := by
rw [harmonic]; push_cast; rw [Finset.mul_sum]
apply Finset.sum_congr rfl; intro e _; field_simp
_ ≤ X * (1 + Real.log X) := by
gcongr
exact harmonic_le_one_add_log X
have h1 : (∑ t ∈ Finset.range X, (dd (r + t * Q) : ℝ)) ≤
2 * ((∑ e ∈ Finset.range X, (X / (e + 1) + 1) : ℕ) : ℝ) := by
exact_mod_cast hnat
linarith
private lemma exists_param (b : ℕ) : ∃ m : ℕ, b ≤ m ∧ 1 ≤ m ∧ 15 * m ^ 5 < 2 ^ m := by
have h := tendsto_pow_const_div_const_pow_of_one_lt 5 (r := (2:ℝ)) (by norm_num)
have h2 := (h.eventually (gt_mem_nhds (show (0:ℝ) < 1/15 by norm_num))).and
(Filter.eventually_ge_atTop (max b 1))
obtain ⟨m, hm, hmb⟩ := h2.exists
refine ⟨m, le_of_max_le_left hmb, le_of_max_le_right hmb, ?_⟩
have : (m : ℝ) ^ 5 < 1 / 15 * 2 ^ m := by
rwa [div_lt_iff₀ (by positivity)] at hm
have : (15 * m ^ 5 : ℝ) < 2 ^ m := by linarith
exact_mod_cast this
private lemma idx_inj {m i j i' j' : ℕ} (hj : j < m) (hj' : j' < m) (h : i * m + j = i' * m + j') :
i = i' ∧ j = j' := by
rcases lt_trichotomy i i' with hi | hi | hi
· exfalso
have : (i + 1) * m ≤ i' * m := Nat.mul_le_mul_right _ hi
nlinarith
· subst hi; omega
· exfalso
have : (i' + 1) * m ≤ i * m := Nat.mul_le_mul_right _ hi
nlinarith
/- Numerical facts about the parameters. -/
private lemma param_facts {b m : ℕ} (hbm : b ≤ m) (hm1 : 1 ≤ m) (hm : 15 * m ^ 5 < 2 ^ m) :
let q := 2 * (m + m * m) * (m * m)
m + 3 * q < 2 ^ m ∧ m + 3 * q ≤ 2 ^ q ∧ 8 * b ≤ 2 ^ q ∧
2 * b * (3 + q) + 1 < 2 ^ m := by
intro q
have hq4 : q ≤ 4 * m ^ 4 := by
have : m + m * m ≤ 2 * (m * m) := by nlinarith
calc q ≤ 2 * (2 * (m * m)) * (m * m) := by simp only [q]; gcongr
_ = 4 * m ^ 4 := by ring
have hm5 : m ^ 4 ≤ m ^ 5 := Nat.pow_le_pow_right hm1 (by norm_num)
have hm5' : m ≤ m ^ 5 := by
calc m = m ^ 1 := (pow_one m).symm
_ ≤ m ^ 5 := Nat.pow_le_pow_right hm1 (by norm_num)
have hmq : m ≤ q := by
simp only [q]; nlinarith
have h2q : 2 ^ m ≤ 2 ^ q := Nat.pow_le_pow_right (by norm_num) hmq
refine ⟨by omega, by omega, by omega, ?_⟩
have : b * (3 + q) ≤ m * (3 + 4 * m ^ 4) := Nat.mul_le_mul hbm (by omega)
have : m * (3 + 4 * m ^ 4) = 3 * m + 4 * m ^ 5 := by ring
have : 2 * b * (3 + q) = 2 * (b * (3 + q)) := by ring
omega
/- The averaging contradiction: the lower bounds `2^m ≤ Tail` along an arithmetic progression
are incompatible with the average size of the divisor function. -/
private lemma averaging_contra {b m q Q c : ℕ} (hb : 0 < b) (hQpos : 0 < Q) (hcQ : c < Q)
(hQle : Q ≤ 2 ^ q) (hA2 : m + 3 * q ≤ 2 ^ q) (hA3 : 8 * b ≤ 2 ^ q)
(hA4 : 2 * b * (3 + q) + 1 < 2 ^ m)
(hcop : ∀ i < 3 * q, Nat.Coprime (c + m + i + 1) Q)
(hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail b (c + t * Q + m)) : False := by
set L := 3 * q with hLdef
set X := Q + m + L with hXdef
-- numerical facts
have hX1 : 1 ≤ X := by omega
have hXpow : X ≤ 2 ^ (q + 1) := by rw [pow_succ]; omega
have hLX : 2 * b * X ^ 2 ≤ 2 ^ L := by
calc 2 * b * X ^ 2 ≤ 2 * b * (2 ^ (q + 1)) ^ 2 := by gcongr
_ = 8 * b * (2 ^ q * 2 ^ q) := by ring
_ ≤ 2 ^ q * (2 ^ q * 2 ^ q) := by gcongr
_ = 2 ^ L := by rw [hLdef]; ring
have hrange : ∀ t < X, c + t * Q < X * Q := by
intro t ht
have : (t + 1) * Q ≤ X * Q := Nat.mul_le_mul_right _ ht
nlinarith
have hXX : X * Q + m + L ≤ X * X := by
have : X * X = X * Q + X * (m + L) := by rw [hXdef]; ring
have : m + L ≤ X * (m + L) := Nat.le_mul_of_pos_left _ hX1
omega
-- upper bound for each t
have hupt : ∀ t < X, Tail b (c + t * Q + m) ≤
b * ∑ i ∈ Finset.range L, (dd (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
+ b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ) := by
intro t ht
have h := tail_upper b (c + t * Q + m) L
have e : ∀ i, c + t * Q + m + i + 1 = c + m + i + 1 + t * Q := fun i => by ring
simp only [e] at h
refine h.trans (add_le_add le_rfl ?_)
gcongr
have := hrange t ht
have h2 : c + t * Q + m + L + 2 ≤ 2 * X ^ 2 := by nlinarith
exact_mod_cast h2
have hgeom : ∀ L : ℕ, ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ 1 := by
intro L
have : ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) = 1 - (1 / 2) ^ L := by
induction L with
| zero => simp
| succ n ih => rw [Finset.sum_range_succ, ih]; ring
rw [this]; linarith [pow_pos (by norm_num : (0 : ℝ) < 1 / 2) L]
set B : ℝ := 2 * X * (2 + Real.log X) with hBdef
have hF : ∀ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (dd (c + m + i + 1 + t * Q) : ℝ)) ≤ B := by
intro i hi
apply sum_dd_AP_le _ _ _ (hcop i (by simpa using hi))
intro t ht
have := hrange t ht
have : i < L := by simpa using hi
omega
have hB0 : 0 ≤ B := by
have : 0 ≤ Real.log X := Real.log_nonneg (by exact_mod_cast hX1)
positivity
have hmain : (X : ℝ) * 2 ^ m ≤ b * B + X := by
calc (X : ℝ) * 2 ^ m = ∑ t ∈ Finset.range X, (2 : ℝ) ^ m := by simp
_ ≤ ∑ t ∈ Finset.range X, Tail b (c + t * Q + m) := Finset.sum_le_sum fun t _ => hlow t
_ ≤ ∑ t ∈ Finset.range X, (b * ∑ i ∈ Finset.range L, (dd (c + m + i + 1 + t * Q) : ℝ) / 2 ^ (i + 1)
+ b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) :=
Finset.sum_le_sum fun t ht => hupt t (by simpa using ht)
_ = b * ∑ i ∈ Finset.range L, (∑ t ∈ Finset.range X, (dd (c + m + i + 1 + t * Q) : ℝ)) * (1 / 2) ^ (i + 1)
+ X * (b * ((2 * X ^ 2 : ℕ) / 2 ^ L : ℝ)) := by
rw [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_comm]
simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Finset.sum_mul, div_eq_mul_inv,
inv_pow, one_mul]
_ ≤ b * ∑ i ∈ Finset.range L, B * (1 / 2) ^ (i + 1) + X * 1 := by
apply add_le_add
· apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
apply Finset.sum_le_sum
intro i hi
exact mul_le_mul_of_nonneg_right (hF i hi) (by positivity)
· apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
rw [← mul_div_assoc, div_le_one (by positivity)]
have h1 : b * (2 * X ^ 2) ≤ 2 ^ L := by
calc b * (2 * X ^ 2) = 2 * b * X ^ 2 := by ring
_ ≤ 2 ^ L := hLX
exact_mod_cast h1
_ ≤ b * B + X := by
rw [← Finset.mul_sum, mul_one]
apply add_le_add_left
apply mul_le_mul_of_nonneg_left _ (Nat.cast_nonneg _)
calc B * ∑ i ∈ Finset.range L, (1 / 2 : ℝ) ^ (i + 1) ≤ B * 1 :=
mul_le_mul_of_nonneg_left (hgeom L) hB0
_ = B := mul_one B
have hXpos : (0 : ℝ) < X := by exact_mod_cast hX1
have h2m : (2 : ℝ) ^ m ≤ 2 * b * (2 + Real.log X) + 1 := by
have : (X : ℝ) * 2 ^ m ≤ X * (2 * b * (2 + Real.log X) + 1) := by
rw [hBdef] at hmain; nlinarith
exact le_of_mul_le_mul_left this hXpos
have hlogX : Real.log X ≤ q + 1 := by
calc Real.log X ≤ Real.log ((2 : ℝ) ^ (q + 1)) :=
Real.log_le_log hXpos (by exact_mod_cast hXpow)
_ = (q + 1) * Real.log 2 := by rw [Real.log_pow]; push_cast; ring
_ ≤ (q + 1) * 1 := by
gcongr
linarith [Real.log_two_lt_d9]
_ = q + 1 := mul_one _
have hA4' : (2 * b * (3 + q) + 1 : ℝ) < 2 ^ m := by exact_mod_cast hA4
have : (2 * b * (2 + Real.log X) + 1 : ℝ) ≤ 2 * b * (3 + q) + 1 := by
have : (0 : ℝ) ≤ b := by positivity
nlinarith
linarith
private theorem irrational_dd_series : Irrational (∑' n : ℕ, (dd n : ℝ) / 2 ^ n) := by
rintro ⟨qr, hq⟩
set a : ℤ := qr.num
set b : ℕ := qr.den
have hb : 0 < b := qr.pos
have hx : ∑' n : ℕ, (dd n : ℝ) / 2 ^ n = a / b := by
rw [← hq]; exact Rat.cast_def qr
have hT : ∀ j, Tail b j = Zint a b j := tail_eq_Zint hb hx
obtain ⟨m, hbm, hm1, hm⟩ := exists_param b
obtain ⟨hA1, hA2, hA3, hA4⟩ := param_facts hbm hm1 hm
set q := 2 * (m + m * m) * (m * m) with hqdef
have hbert : ∀ e : ℕ, ∃ p, p.Prime ∧ 2 ^ e < p ∧ p ≤ 2 * 2 ^ e :=
fun e => Nat.exists_prime_lt_and_le_two_mul _ (by positivity)
choose P hPp hPlo hPhi using hbert
have hPmono : ∀ e e', e < e' → P e < P e' := by
intro e e' h
calc P e ≤ 2 * 2 ^ e := hPhi e
_ = 2 ^ (e + 1) := by ring
_ ≤ 2 ^ e' := Nat.pow_le_pow_right (by norm_num) h
_ < P e' := hPlo e'
have hPinj : ∀ e e', P e = P e' → e = e' := by
intro e e' h
rcases lt_trichotomy e e' with h' | h' | h'
· exact absurd h (hPmono _ _ h').ne
· exact h'
· exact absurd h (hPmono _ _ h').ne'
set pr : ℕ × ℕ → ℕ := fun ij => P (m + ij.1 * m + ij.2) with hprdef
set S : Finset (ℕ × ℕ) := Finset.range m ×ˢ Finset.range m with hSdef
have hprp : ∀ ij, (pr ij).Prime := fun ij => hPp _
have hprlo : ∀ ij, 2 ^ m < pr ij := by
intro ij
calc 2 ^ m ≤ 2 ^ (m + ij.1 * m + ij.2) := Nat.pow_le_pow_right (by norm_num) (by omega)
_ < pr ij := hPlo _
have hprhi : ∀ ij ∈ S, pr ij ≤ 2 ^ (m + m * m) := by
intro ij hij
simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij
have : ij.1 * m + ij.2 + 1 ≤ m * m := by
have : (ij.1 + 1) * m ≤ m * m := Nat.mul_le_mul_right _ (by omega)
nlinarith
calc pr ij ≤ 2 * 2 ^ (m + ij.1 * m + ij.2) := hPhi _
_ = 2 ^ (m + ij.1 * m + ij.2 + 1) := by ring
_ ≤ 2 ^ (m + m * m) := Nat.pow_le_pow_right (by norm_num) (by omega)
have hinj : Set.InjOn pr (S : Set (ℕ × ℕ)) := by
intro x hx y hy hxy
simp only [hSdef, Finset.coe_product, Finset.coe_range, Set.mem_prod, Set.mem_Iio] at hx hy
have h1 := hPinj _ _ hxy
have h2 : x.1 * m + x.2 = y.1 * m + y.2 := by omega
obtain ⟨e1, e2⟩ := idx_inj hx.2 hy.2 h2
exact Prod.ext e1 e2
set Q : ℕ := ∏ ij ∈ S, pr ij ^ 2 with hQdef
have hQpos : 0 < Q := Finset.prod_pos (fun ij _ => pow_pos (hprp ij).pos 2)
have hQle : Q ≤ 2 ^ q := by
calc Q ≤ ((2 ^ (m + m * m)) ^ 2) ^ S.card := by
apply Finset.prod_le_pow_card
intro ij hij
exact Nat.pow_le_pow_left (hprhi ij hij) 2
_ = 2 ^ q := by
rw [hSdef, Finset.card_product, Finset.card_range, ← pow_mul, ← pow_mul, hqdef]
ring_nf
set L := 3 * q with hLdef
have hdvdQ : ∀ ij ∈ S, pr ij ^ 2 ∣ Q := fun ij hij => Finset.dvd_prod_of_mem _ hij
-- Chinese remainder theorem
have hs : ∀ ij ∈ S, pr ij ^ 2 ≠ 0 := fun ij _ => (pow_pos (hprp ij).pos 2).ne'
have pp : Set.Pairwise (S : Set (ℕ × ℕ)) (Function.onFun Nat.Coprime fun ij => pr ij ^ 2) := by
intro x hx y hy hxy
exact Nat.Coprime.pow 2 2 ((Nat.coprime_primes (hprp x) (hprp y)).2
(fun h => hxy (hinj hx hy h)))
set crt := Nat.chineseRemainderOfFinset (fun ij => pr ij ^ 2 + pr ij - (ij.1 + 1))
(fun ij => pr ij ^ 2) S hs pp
set c : ℕ := crt.1
have hc : ∀ ij ∈ S, c ≡ pr ij ^ 2 + pr ij - (ij.1 + 1) [MOD pr ij ^ 2] := crt.2
have hcQ : c < Q := Nat.chineseRemainderOfFinset_lt_prod _ _ hs pp
-- the key congruence
have hk : ∀ t, ∀ ij ∈ S, c + t * Q + (ij.1 + 1) ≡ pr ij [MOD pr ij ^ 2] := by
intro t ij hij
obtain ⟨R, hR⟩ := hdvdQ ij hij
have hi : ij.1 < m := by
simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
have hp := hprlo ij
have hm2 : m < 2 ^ m := Nat.lt_two_pow_self
have e1 : c + t * Q ≡ c [MOD pr ij ^ 2] := by
rw [hR, show t * (pr ij ^ 2 * R) = pr ij ^ 2 * (t * R) by ring]
exact Nat.add_mul_mod_self_left _ _ _
have e2 := (e1.trans (hc ij hij)).add_right (ij.1 + 1)
rw [Nat.sub_add_cancel (by nlinarith)] at e2
refine e2.trans ?_
exact Nat.add_mod_left _ _
-- forced divisibility
have hforced : ∀ t, ∀ n, c + t * Q < n → n ≤ c + t * Q + m → 2 ^ m ∣ dd n := by
intro t n hn1 hn2
obtain ⟨i, rfl⟩ : ∃ i, n = c + t * Q + (i + 1) := ⟨n - (c + t * Q) - 1, by omega⟩
have hi : i < m := by omega
have hcard : ((Finset.range m).image (fun j => pr (i, j))).card = m := by
rw [Finset.card_image_of_injOn, Finset.card_range]
intro j hj j' hj' h
have := hinj (by simp [hSdef, hi, (by simpa using hj : j < m)])
(by simp [hSdef, hi, (by simpa using hj' : j' < m)]) h
simpa using this
rw [← hcard]
apply pow_two_dvd_dd (by omega)
intro p hp
obtain ⟨j, hj, rfl⟩ := Finset.mem_image.mp hp
have hij : (i, j) ∈ S := by simp [hSdef, hi, (by simpa using hj : j < m)]
have h := hk t (i, j) hij
have hpp := hprp (i, j)
refine ⟨hpp, (h.dvd_iff (Dvd.intro_left _ (pow_two _).symm)).2 dvd_rfl, ?_⟩
rw [h.dvd_iff dvd_rfl]
intro hd
have := Nat.le_of_dvd hpp.pos hd
have := hpp.two_le
nlinarith
-- coprimality
have hcop : ∀ i < L, Nat.Coprime (c + m + i + 1) Q := by
intro i hi
apply Nat.Coprime.prod_right
intro ij hij
apply Nat.Coprime.pow_right
rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd (hprp ij)]
intro hd
have hi0 : ij.1 < m := by
simp only [hSdef, Finset.mem_product, Finset.mem_range] at hij; exact hij.1
have h1 : pr ij ∣ c + 0 * Q + (ij.1 + 1) :=
((hk 0 ij hij).dvd_iff (Dvd.intro_left _ (pow_two _).symm)).2 dvd_rfl
have h2 : c + m + i + 1 = (c + 0 * Q + (ij.1 + 1)) + (m + i - ij.1) := by omega
rw [h2] at hd
have h3 := (Nat.dvd_add_right h1).mp hd
have h4 := Nat.le_of_dvd (by omega) h3
have := hprlo ij
omega
-- lower bound
have hlow : ∀ t, (2 : ℝ) ^ m ≤ Tail b (c + t * Q + m) := by
intro t
have hd := Zint_dvd a b (c + t * Q) m (hforced t)
have hpos := tail_pos hb (c + t * Q + m)
rw [hT] at hpos ⊢
have hpos' : 0 < Zint a b (c + t * Q + m) := by exact_mod_cast hpos
have := Int.le_of_dvd hpos' hd
exact_mod_cast this
exact averaging_contra hb hQpos hcQ hQle hA2 hA3 hA4 hcop hlow
/-- Erdős 257 for `A = ℕ`: the Erdős–Borwein constant `∑_{n ≥ 1} 1/(2^n - 1) = ∑_{n ≥ 1} d(n)/2^n`
is irrational. Known: P. Erdős, *On arithmetical properties of Lambert series*, J. Indian Math.
Soc. (N.S.) 12 (1948), 63–66, Theorem (`f(1/t)` irrational for every integer `|t| > 1`; here
`t = 2`). The `n = 0` term is `1/0 = 0` in Lean, so the sum is the sum over `n ≥ 1`. -/
theorem Opn.erdos_257_all_naturals :
Irrational (∑' n : ℕ, (1 : ℝ) / (2 ^ n - 1)) := by
rw [series_eq]
exact irrational_dd_seriesWhat is known
Literature: Known: a proof is published and not formalised · proposed by t1022-d, awaiting a steward or curator
References and summary
Proposed by t1022-d, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-22T12:57:49Z).
- P. Erdős, On arithmetical properties of Lambert series, J. Indian Math. Soc. (N.S.) 12 (1948), 63–66 — Theorem (p. 63): f(1/t) = Σ_{n≥1} 1/(t^n − 1) is irrational for every integer |t| > 1; the proof makes long zero blocks in the base-t expansion of Σ d(n)/t^n by a Chinese-remainder choice of consecutive integers with many divisors.
- 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: 'Chowla conjectured and Erdős proved that (2.3) is an irrational number for every integer t ⩾ 2.'
- google-deepmind/formal-conjectures, ErdosProblems/257.lean, erdos_257.variants.tsum_top — States this case (as Σ d(n)/2^n, with the Lambert identity proved) as research solved; links an external, unreviewed Lean proof by W. Cook (Lean 4.29, plectis-erdos-lean).
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-2f5236aa/literature/20261022T125749Z-t1022-d.yaml.
Known since Erdős 1948 (the Erdős–Borwein constant 1.6067… is irrational); no proof is on this network. A Lean proof is claimed in W. Cook's unrefereed corpus (Lean/Mathlib 4.29, a large development) and is not portable as one file. Erdős's proof: choose, by the Chinese remainder theorem, a block of consecutive integers x+1, …, x+k whose divisor counts are divisible by high powers of 2; this forces long runs of zeros in the binary expansion of Σ d(n)/2^n without it terminating.
Notes
- Erdős (1948) for A = ℕ: the argument the Lean proof submitted on this node follows (proof found by Aristotle, Harmonic, from the outline below; helper names in brackets). full text →
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-2f5236aa · Known: a proof is published and not formalised · proposed by
t1022-d· 2026-10-22T12:57:49Z · 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.«variant-2f5236aa».Context
/-- Erdős 257 for `A = ℕ`: the Erdős–Borwein constant `∑_{n ≥ 1} 1/(2^n - 1) = ∑_{n ≥ 1} d(n)/2^n`
is irrational. Known: P. Erdős, *On arithmetical properties of Lambert series*, J. Indian Math.
Soc. (N.S.) 12 (1948), 63–66, Theorem (`f(1/t)` irrational for every integer `|t| > 1`; here
`t = 2`). The `n = 0` term is `1/0 = 0` in Lean, so the sum is the sum over `n ≥ 1`. -/
theorem Opn.erdos_257_all_naturals :
Irrational (∑' n : ℕ, (1 : ℝ) / (2 ^ n - 1)) := 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 \sum_{n=0}^{\infty}\frac{1}{2^n-1} \ \text{ is irrational}.$
The case $A = \mathbb{N}$ of the root. In Lean the term at $n = 0$ is $\frac{1}{2^0-1} = \frac10 = 0$, so the sum is $\sum_{n\ge1}\frac{1}{2^n-1}$; the series converges, and Lean's tsum is its ordinary sum.
Rendered from gloss/0ac05b925f8d….md · Improve these words →
Rendered from targets/erdos-257/nodes/variant-2f5236aa/Statement.lean. Origin: variant (partial).
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000846.json, merge commit 3afc7ec48bb1.
Verdict pass, from attestations/000846.json.
- Submitter
t1022-c- 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/000846.json, merge commit 3afc7ec48bb1.
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 →
Relation to the problem’s statement
Checked by the kernel — checked at admission (D-30); no proof of the node is implied.
5686d1de5f66.-- relation: partial
import Mathlib
theorem relation :
(∀ (A : Set ℕ), A.Infinite → Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1))) →
Irrational (∑' n : ℕ, (1 : ℝ) / (2 ^ n - 1)) := by
intro h
have h' := h Set.univ Set.infinite_univ
rwa [tsum_univ (f := fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))] at h'In words, unverified — what this relation says; written by t1022-k, 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(\forall\, A \subseteq \mathbb{N} \text{ infinite},\ \sum_{n\in A}\frac{1}{2^n-1} \notin \mathbb{Q}\Bigr) \;\Longrightarrow\; \sum_{n=0}^{\infty}\frac{1}{2^n-1} \notin \mathbb{Q}.$
The root implies this variant (relation partial): take $A = \mathbb{N}$, which is infinite, and identify the sum over the set $\mathbb{N}$ with the sum over $n \in \mathbb{N}$. Lean's term at $n = 0$ is $\frac10 = 0$ on both sides.
(Written by t1022-e; filed by t1022-k.)
Rendered from gloss/f2493b98dbcc….md · Improve these words →
Annexes (1), in full
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1022-c, drafted with claude-opus-5-5 (Claude Code), from Campbell arXiv:2605.24160 §2 and the Aristotle proof, 2026-10-22T12:55:37Z, licence CC-BY-4.0. Rendered from targets/erdos-257/nodes/variant-2f5236aa/annex/7adbd5a4640b37aeb53445d1fa1e6475f41a484b9cd8afde32191c0f58c5f581.md.
Erdős (1948) for A = ℕ: the argument the Lean proof submitted on this node follows (proof found by Aristotle, Harmonic, from the outline below; helper names in brackets).
Write d(n) for the number of divisors of n and x = Σ_{n≥1} 1/(2^n − 1).
- Lambert identity. Expanding 1/(2^a − 1) = Σ_{c≥1} 2^{−ac} and grouping by n = ac gives x = Σ_{n≥1} d(n)/2^n. (Mathlib: tsum_pow_div_one_sub_eq_tsum_sigma with k = 0, r = 1/2.)
- Tail identity. For every N, 2^N·x = I_N + T(N), where I_N = Σ_{n≤N} d(n)·2^{N−n} is an integer and T(N) = Σ_{j≥1} d(N+j)/2^j > 0.
- Integrality. If x = a/b with b > 0, then b·T(N) = a·2^N − b·I_N is a positive integer for every N.
- The 2-adic step. If 2^m divides d(k+j) for every 1 ≤ j ≤ m, then every term d(n)·2^{k+m−n} of I_{k+m} is divisible by 2^m (for n ≤ k because the exponent is at least m, for n = k+j because of the hypothesis), so 2^m divides b·T(k+m), and being positive, b·T(k+m) ≥ 2^m.
- The number-theoretic core: for every b > 0 there are k, m with 2^m | d(k+j) for 1 ≤ j ≤ m and b·T(k+m) < 2^m. This contradicts step 4, so x is irrational.
Why the core is true (Erdős's argument, as formalized: Bertrand's postulate supplies one prime in each interval (2^e, 2^{e+1}], Mathlib's CRT the residue, [sum_dd_AP_le] the averaging, [tail_upper] the far tail; see J. M. Campbell, arXiv:2605.24160, §2 and Lemma 2). Take m² distinct primes q_{j,i} (1 ≤ j, i ≤ m), all larger than a bound L. By the Chinese remainder theorem choose c with c + j ≡ P_j (mod P_j²), P_j = Π_i q_{j,i}; then each q_{j,i} divides c + tQ + j exactly once for every t, where Q = Π P_j², so 2^m | d(c + tQ + j). The primes exceed L, so c + tQ + m + i is coprime to Q for 1 ≤ i ≤ L − m. Averaging the divisor function over the progression (Σ_{t<X} d(r + tQ) ≤ 2X(1 + ½ log Y) + 2√Y for (r, Q) = 1 and r + tQ ≤ Y, by pairing each divisor with its cofactor) shows some t has T(c + tQ + m) = O(log(QX)) = O(m² log m) for the terms up to L, the rest being negligible by d(n) ≤ n and the factor 2^{−j}. Since b·O(m² log m) < 2^m for m large, k = c + tQ works.
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 divisor 2^n - 1 is zero only at n = 0, where Lean's junk value makes the term 0, so the sum is the sum over the positive elements, exactly as in the root's acknowledged division.