Irrationality of the prime indicator in base 2

variant-09e95e7a

proved

A related variant. not yet signed as pertinent to the target (D-30 v3.12)

$\displaystyle \sum_{n=0}^{\infty}\bigl[n\ \text{prime}\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

The real number whose binary expansion has a 1 in place n exactly when n is prime, the sum over n ≥ 0 of (1/2)^n for prime n and 0 otherwise, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.

unverified · history

Lean

theorem Opn.erdos_69_prime_indicator :
    Irrational (∑' n : ℕ, if n.Prime then (1 / 2 : ℝ) ^ n else 0) := by
  sorry

Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

Explainer

Informal account, unverified — unverified prose about a kernel-checked proof; shown section by section, each labelled with who drafted, wrote or verified it (D-3 v3.31).

Unverified: explainer, its words from explainer/3e48fdc8776d….md, machine-drafted by anthropic/claude-opus-5.5 (opn-drafter), 2026-10-05.

Idea and method

Draft · drafted, by the model named above

The claim is that the real number $\sum_{n\ge 0} f(n)$ is irrational. The case splits recorded in the outline indicate that $f(n)$ is $(1/2)^n$ when $n$ is prime and $0$ otherwise. The proof is the classical argument by contradiction for sums of this kind.

Suppose the sum equals a rational $q$ with denominator $k$. Then go far enough out that a run of $k$ consecutive integers contains no primes. A factorial-shifted block works: each $j+N+1$ with $j<k$ has the proper divisor $j+2$.

Split the series into three parts:

a finite head up to index $N$, which becomes an integer after multiplying by $2^N$;
the block of $k$ vanishing terms;
a tail $R$.

Multiplying by $2^N k$ turns the identity $q = \text{head} + R$ into an integer equal to $k\,2^N R$. That quantity is strictly positive, because a prime lies beyond the block. It is also strictly less than $1$, because the tail is dominated by a geometric series and $k<2^k$. No integer lies strictly between $0$ and $1$.

Read it step by step (7 more sections)

Bounds on the terms and convergence

Draft · drafted, by the model named above

f_nonneg records $0 \le f(n)$ for all $n$.

f_le records $f(n) \le (1/2)^n$, by a case split on the defining condition of $f$:

In the first case (f_le.s1) the goal is $(1/2)^n \le (1/2)^n$, closed by reflexivity.
In the second case (f_le.s2) the goal is $0 \le (1/2)^n$, which is routine positivity.

From these two bounds, hs obtains that $f$ is summable. It uses the comparison test ("Comparison test of convergence of series of non-negative real numbers") against the geometric series $\sum (1/2)^n$, whose summability is summable_geometric_of_lt_one.

After these steps the goal is still that $\sum_n f(n)$ is irrational.

A block of $k$ vanishing terms

Draft · drafted, by the model named above

From kpos on, the goal is False, so the proof proceeds by contradiction. The outline does not record the step that sets this up. From here on it works with:

a rational $q$;
a natural number $k$, which a later step (hqk) shows satisfies $q\cdot k = \operatorname{num}(q)$;
natural numbers $N$ and $Z$;
a real number $R$.

kpos records $0<k$.

comp claims that $f(j+N+1)=0$ for every $j<k$. (The statement is written with the index $j + k\cdot 0 + N+1$.) Its first child hd shows $j+2 \mid j+N+1$ from two facts:

comp.hd.this gives $j+2 \mid (k+1)!$, via Nat.dvd_factorial, since $j+2\le k+1$.
comp.hd.e gives the identity $j+N+1 = (k+1)! + (j+2)$.

Divisibility of the sum then follows from dvd_add and dvd_rfl.

Two cases then close the goal False, which concerns $j+N+1$ being prime:

comp.s2 is routine (linear arithmetic).
comp.s3 uses comp.s3.this, the positivity $0<(k+1)!$ from Nat.factorial_pos.

With primality excluded, comp evaluates $f$ by its "else" branch (if_neg) to $0$.

Splitting the series

Draft · drafted, by the model named above

hg records that the shifted series $i\mapsto f(i+N+1)$ is summable, by summable_nat_add_iff. hg' records the same for $i \mapsto f(i+k+N+1)$, via its child hg'.this and reassociation of the index.

The series is then split twice, both times by Summable.sum_add_tsum_nat_add:

split1 gives $\sum_{i<N+1} f(i) + \sum_i f(i+N+1) = \sum_i f(i)$.
split2 gives $\sum_{i<k} f(i+N+1) + \sum_i f(i+k+N+1) = \sum_i f(i+N+1)$.

zero_part shows that the middle finite sum $\sum_{i<k} f(i+N+1)$ is $0$, by Finset.sum_eq_zero. Each term vanishes by zero_part.this, which applies comp to $j<k$ (membership in $\{0,\dots,k-1\}$ via Finset.mem_range).

split2' then concludes $\sum_i f(i+N+1) = R$, using zero_add. Here $R$ is the tail $\sum_i f(i+k+N+1)$.

The tail is positive

Draft · drafted, by the model named above

Rpos claims $0<R$.

Let $p$ be a prime with $k+N+1 \le p$, obtained in Rpos.s1 from Euclid's theorem on the infinitude of primes (Nat.exists_infinite_primes). Rpos.hpi is the routine identity $p-(k+N+1)+k+N+1 = p$. This places $p$ as the index of a term of the tail.

That term is evaluated by the "then" branch (if_pos) and is positive. Since all terms of the tail are nonnegative, $R>0$.

The tail is small

Draft · drafted, by the model named above

geo records that $i\mapsto (1/2)^{i+k+N+1}$ is summable. Its child geo.this shows this for the reassociated exponent $i+(k+N+1)$, using summable_nat_add_iff and summable_geometric_of_lt_one.

Rle claims $R \le (1/2)^{k+N+1}\cdot 2$, by a two-step calculation:

Rle.s1 gives $R \le \sum_i (1/2)^{i+k+N+1}$ by termwise comparison (Summable.tsum_le_tsum).
Rle.s2 evaluates this sum as $(1/2)^{k+N+1}\cdot 2$. It uses pow_add to factor out $(1/2)^{k+N+1}$, then tsum_mul_right, then tsum_geometric_two, together with add_assoc and mul_comm.

key claims $2^N\bigl((1/2)^{k+N+1}\cdot 2\bigr) = (1/2)^k$:

key.h1 records $2^N(1/2)^N = 1$ (via mul_pow).
key.s2 rewrites the left side as $(1/2)^k\,\bigl(2^N (1/2)^N\bigr)\,\bigl(\tfrac12\cdot 2\bigr)$ (via pow_add and pow_succ).
key.s3 finishes the calculation. The outline records no claim for this step.

The head is an integer after scaling

Draft · drafted, by the model named above

hZ' claims $2^N \sum_{i<N+1} f(i) = Z$ as real numbers. It distributes $2^N$ over the sum (Finset.mul_sum) and compares termwise (Finset.sum_congr). For each $i$ in the range, with $i\le N$ recorded in hZ'.hi', the goal becomes $$2^N f(i) = \begin{cases} 2^{N-i} & \text{if } i \text{ is prime},\\ 0 & \text{otherwise.}\end{cases}$$

In the prime case (hZ'.s2) the goal is $2^N(1/2)^i = 2^{N-i}$. It follows from hZ'.s2.e, namely $2^N = 2^{N-i}\,2^i$ (via pow_add and Nat.sub_add_cancel), together with mul_assoc and mul_pow.

The remaining case hZ'.s3, $2^N\cdot 0 = 0$, is routine simplification.

Steps

14 steps

hqk have (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ)
hx have (↑q : ℝ) = ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + R
hm have (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((2 : ℝ) ^ N * R)
mpos have (0 : ℝ) < (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ)
mpos.this have (0 : ℝ) < (↑k : ℝ)
mlt have (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ)
mlt.h2 have (2 : ℝ) ^ N * R ≤ (1 / 2 : ℝ) ^ k
mlt.hk2 have (↑k : ℝ) < (2 : ℝ) ^ k
mlt.hk0 have (0 : ℝ) ≤ (↑k : ℝ)
mlt.s4 calc (↑k : ℝ) * ((2 : ℝ) ^ N * R) ≤ (↑k : ℝ) * (1 / 2 : ℝ) ^ k
mlt.s5 calc
mlt.s6 calc
i1 have (0 : ℤ) < (2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)
i2 have (2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ)

An integer strictly between $0$ and $1$

Draft · drafted, by the model named above

hqk records $q\cdot k = \operatorname{num}(q)$ (Rat.mul_den_eq_num). hx records $q = \sum_{i<N+1} f(i) + R$.

From these, hm obtains for the integer $m = 2^N\operatorname{num}(q) - kZ$ the identity $$m = k\,(2^N R) \quad\text{in } \mathbb{R}.$$

mpos shows $m>0$. With mpos.this giving $0<k$ as a real number and $R>0$ from before, the goal reduces to $0 < k\,(2^N R)$.

mlt shows $m<1$, so the goal becomes $k\,(2^N R) < 1$. Its children supply three inputs:

mlt.h2 gives $2^N R \le (1/2)^k$, using mul_le_mul_of_nonneg_left.
mlt.hk2 gives $k < 2^k$ (Nat.lt_two_pow_self).
mlt.hk0, the bound $0\le k$, is routine positivity.

The chain then runs as follows:

mlt.s4 gives $k(2^N R) \le k(1/2)^k$.
mlt.s5 rewrites the right side as $k/2^k$ (one_div_pow, mul_one_div).
mlt.s6 gives $k/2^k<1$ (div_lt_one).

Finally, i1 and i2 transfer the two bounds to the integers: $0 < 2^N\operatorname{num}(q) - kZ$ and $2^N\operatorname{num}(q) - kZ < 1$. The remaining goal is False. No integer satisfies both bounds, so the assumption that the sum is rational is refuted.

Improve these words →

History: 1 version on record

2026-10-05 · machine-drafted by anthropic/claude-opus-5.5 (opn-drafter) · not signed · current · explainer/3e48fdc8776d….md · the first version of its chain
Read this version
Idea and method
The claim is that the real number $\sum_{n\ge 0} f(n)$ is irrational. The case splits recorded in the outline indicate that $f(n)$ is $(1/2)^n$ when $n$ is prime and $0$ otherwise. The proof is the classical argument by contradiction for sums of this kind.

Suppose the sum equals a rational $q$ with denominator $k$. Then go far enough out that a run of $k$ consecutive integers contains no primes. A factorial-shifted block works: each $j+N+1$ with $j<k$ has the proper divisor $j+2$.

Split the series into three parts:
- a finite head up to index $N$, which becomes an integer after multiplying by $2^N$;
- the block of $k$ vanishing terms;
- a tail $R$.
Multiplying by $2^N k$ turns the identity $q = \text{head} + R$ into an integer equal to $k\,2^N R$. That quantity is strictly positive, because a prime lies beyond the block. It is also strictly less than $1$, because the tail is dominated by a geometric series and $k<2^k$. No integer lies strictly between $0$ and $1$.
Bounds on the terms and convergence (f_nonneg f_le f_le.s1 f_le.s2 hs)
f_nonneg records $0 \le f(n)$ for all $n$.

f_le records $f(n) \le (1/2)^n$, by a case split on the defining condition of $f$:
- In the first case (f_le.s1) the goal is $(1/2)^n \le (1/2)^n$, closed by reflexivity.
- In the second case (f_le.s2) the goal is $0 \le (1/2)^n$, which is routine positivity.
From these two bounds, hs obtains that $f$ is summable. It uses the comparison test ("Comparison test of convergence of series of non-negative real numbers") against the geometric series $\sum (1/2)^n$, whose summability is summable_geometric_of_lt_one.

After these steps the goal is still that $\sum_n f(n)$ is irrational.
A block of $k$ vanishing terms (kpos comp comp.hd comp.hd.this comp.hd.e comp.s2 comp.s3 comp.s3.this)
From kpos on, the goal is False, so the proof proceeds by contradiction. The outline does not record the step that sets this up. From here on it works with:
- a rational $q$;
- a natural number $k$, which a later step (hqk) shows satisfies $q\cdot k = \operatorname{num}(q)$;
- natural numbers $N$ and $Z$;
- a real number $R$.
kpos records $0<k$.

comp claims that $f(j+N+1)=0$ for every $j<k$. (The statement is written with the index $j + k\cdot 0 + N+1$.) Its first child hd shows $j+2 \mid j+N+1$ from two facts:
- comp.hd.this gives $j+2 \mid (k+1)!$, via Nat.dvd_factorial, since $j+2\le k+1$.
- comp.hd.e gives the identity $j+N+1 = (k+1)! + (j+2)$.
Divisibility of the sum then follows from dvd_add and dvd_rfl.

Two cases then close the goal False, which concerns $j+N+1$ being prime:
- comp.s2 is routine (linear arithmetic).
- comp.s3 uses comp.s3.this, the positivity $0<(k+1)!$ from Nat.factorial_pos.
With primality excluded, comp evaluates $f$ by its "else" branch (if_neg) to $0$.
Splitting the series (hg hg' hg'.this split1 split2 zero_part zero_part.this split2')
hg records that the shifted series $i\mapsto f(i+N+1)$ is summable, by summable_nat_add_iff. hg' records the same for $i \mapsto f(i+k+N+1)$, via its child hg'.this and reassociation of the index.

The series is then split twice, both times by Summable.sum_add_tsum_nat_add:
- split1 gives $\sum_{i<N+1} f(i) + \sum_i f(i+N+1) = \sum_i f(i)$.
- split2 gives $\sum_{i<k} f(i+N+1) + \sum_i f(i+k+N+1) = \sum_i f(i+N+1)$.
zero_part shows that the middle finite sum $\sum_{i<k} f(i+N+1)$ is $0$, by Finset.sum_eq_zero. Each term vanishes by zero_part.this, which applies comp to $j<k$ (membership in $\{0,\dots,k-1\}$ via Finset.mem_range).

split2' then concludes $\sum_i f(i+N+1) = R$, using zero_add. Here $R$ is the tail $\sum_i f(i+k+N+1)$.
The tail is positive (Rpos Rpos.s1 Rpos.hpi)
Rpos claims $0<R$.

Let $p$ be a prime with $k+N+1 \le p$, obtained in Rpos.s1 from Euclid's theorem on the infinitude of primes (Nat.exists_infinite_primes). Rpos.hpi is the routine identity $p-(k+N+1)+k+N+1 = p$. This places $p$ as the index of a term of the tail.

That term is evaluated by the "then" branch (if_pos) and is positive. Since all terms of the tail are nonnegative, $R>0$.
The tail is small (geo geo.this Rle Rle.s1 Rle.s2 key key.h1 key.s2 key.s3)
geo records that $i\mapsto (1/2)^{i+k+N+1}$ is summable. Its child geo.this shows this for the reassociated exponent $i+(k+N+1)$, using summable_nat_add_iff and summable_geometric_of_lt_one.

Rle claims $R \le (1/2)^{k+N+1}\cdot 2$, by a two-step calculation:
- Rle.s1 gives $R \le \sum_i (1/2)^{i+k+N+1}$ by termwise comparison (Summable.tsum_le_tsum).
- Rle.s2 evaluates this sum as $(1/2)^{k+N+1}\cdot 2$. It uses pow_add to factor out $(1/2)^{k+N+1}$, then tsum_mul_right, then tsum_geometric_two, together with add_assoc and mul_comm.
key claims $2^N\bigl((1/2)^{k+N+1}\cdot 2\bigr) = (1/2)^k$:
- key.h1 records $2^N(1/2)^N = 1$ (via mul_pow).
- key.s2 rewrites the left side as $(1/2)^k\,\bigl(2^N (1/2)^N\bigr)\,\bigl(\tfrac12\cdot 2\bigr)$ (via pow_add and pow_succ).
- key.s3 finishes the calculation. The outline records no claim for this step.
The head is an integer after scaling (hZ' hZ'.hi' hZ'.s2 hZ'.s2.e hZ'.s3)
hZ' claims $2^N \sum_{i<N+1} f(i) = Z$ as real numbers. It distributes $2^N$ over the sum (Finset.mul_sum) and compares termwise (Finset.sum_congr). For each $i$ in the range, with $i\le N$ recorded in hZ'.hi', the goal becomes $$2^N f(i) = \begin{cases} 2^{N-i} & \text{if } i \text{ is prime},\\ 0 & \text{otherwise.}\end{cases}$$

In the prime case (hZ'.s2) the goal is $2^N(1/2)^i = 2^{N-i}$. It follows from hZ'.s2.e, namely $2^N = 2^{N-i}\,2^i$ (via pow_add and Nat.sub_add_cancel), together with mul_assoc and mul_pow.

The remaining case hZ'.s3, $2^N\cdot 0 = 0$, is routine simplification.
An integer strictly between $0$ and $1$ (hqk hx hm mpos mpos.this mlt mlt.h2 mlt.hk2 mlt.hk0 mlt.s4 mlt.s5 mlt.s6 i1 i2)
hqk records $q\cdot k = \operatorname{num}(q)$ (Rat.mul_den_eq_num). hx records $q = \sum_{i<N+1} f(i) + R$.

From these, hm obtains for the integer $m = 2^N\operatorname{num}(q) - kZ$ the identity $$m = k\,(2^N R) \quad\text{in } \mathbb{R}.$$

mpos shows $m>0$. With mpos.this giving $0<k$ as a real number and $R>0$ from before, the goal reduces to $0 < k\,(2^N R)$.

mlt shows $m<1$, so the goal becomes $k\,(2^N R) < 1$. Its children supply three inputs:
- mlt.h2 gives $2^N R \le (1/2)^k$, using mul_le_mul_of_nonneg_left.
- mlt.hk2 gives $k < 2^k$ (Nat.lt_two_pow_self).
- mlt.hk0, the bound $0\le k$, is routine positivity.
The chain then runs as follows:
- mlt.s4 gives $k(2^N R) \le k(1/2)^k$.
- mlt.s5 rewrites the right side as $k/2^k$ (one_div_pow, mul_one_div).
- mlt.s6 gives $k/2^k<1$ (div_lt_one).
Finally, i1 and i2 transfer the two bounds to the integers: $0 < 2^N\operatorname{num}(q) - kZ$ and $2^N\operatorname{num}(q) - kZ < 1$. The remaining goal is False. No integer satisfies both bounds, so the assumption that the sum is rational is refuted.

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000224.json, merge commit 40da7e649495.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 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.

f_nonneg have ∀ (n : ℕ), (0 : ℝ) ≤ f n
Leaves Irrational (tsum f), with f_nonneg : ∀ (n : ℕ), (0 : ℝ) ≤ f n.
Lean, lines 17–18
```
  have f_nonneg : ∀ n, 0 ≤ f n := fun n => by
    simp only [hf]; split_ifs <;> positivity
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 17–18 at 40da7e649495 ↗
f_le have ∀ (n : ℕ), f n ≤ (1 / 2 : ℝ) ^ n
Leaves Irrational (tsum f), with f_le : ∀ (n : ℕ), f n ≤ (1 / 2 : ℝ) ^ n.
Lean, lines 19–22
```
  have f_le : ∀ n, f n ≤ (1 / 2 : ℝ) ^ n := fun n => by
    simp only [hf]; split_ifs
    · exact le_rfl
    · positivity
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 19–22 at 40da7e649495 ↗
1. f_le.s1 case
  Leaves (1 / 2 : ℝ) ^ n ≤ (1 / 2 : ℝ) ^ n.
  Uses library le_rfl.
  Lean, line 21
  · exact le_rfl
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 21 at 40da7e649495 ↗
2. f_le.s2 case routine: positivity
  Leaves (0 : ℝ) ≤ (1 / 2 : ℝ) ^ n.
  Lean, line 22
  · positivity
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 22 at 40da7e649495 ↗
hs have Summable f
Leaves Irrational (tsum f), with hs : Summable f.
Uses library Summable, Summable.of_nonneg_of_le, summable_geometric_of_lt_one.
Lean, lines 23–25
```
  have hs : Summable f :=
    Summable.of_nonneg_of_le f_nonneg f_le
      (summable_geometric_of_lt_one (by norm_num) (by norm_num))
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 23–25 at 40da7e649495 ↗
kpos have (0 : ℕ) < k
Leaves False, with kpos : (0 : ℕ) < k.
Lean, line 28
```
  have kpos : 0 < k := q.den_pos
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 28 at 40da7e649495 ↗
comp have ∀ j < k, f (j + k * (0 : ℕ) + (N + (1 : ℕ))) = (0 : ℝ)
Leaves False, with comp : ∀ j < k, f (j + k * (0 : ℕ) + (N + (1 : ℕ))) = (0 : ℝ).
Uses library MulZeroClass.mul_zero, add_zero, if_neg.
Lean, lines 31–43
```
  have comp : ∀ j, j < k → f (j + k * 0 + (N + 1)) = 0 := by
    intro j hj
    simp only [hf, mul_zero, add_zero]
    rw [if_neg]
    intro hp
    have hd : (j + 2) ∣ j + (N + 1) := by
      have : (j + 2) ∣ (k + 1).factorial := Nat.dvd_factorial (by omega) (by omega)
      have e : j + (N + 1) = (k + 1).factorial + (j + 2) := by rw [hN]; ring
      rw [e]; exact dvd_add this dvd_rfl
    rcases hp.eq_one_or_self_of_dvd _ hd with h | h
    · omega
    · have : 0 < (k + 1).factorial := Nat.factorial_pos _
      rw [hN] at h; omega
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 31–43 at 40da7e649495 ↗
1. comp.hd have j + (2 : ℕ) ∣ j + (N + (1 : ℕ))
  Leaves False, with hd : j + (2 : ℕ) ∣ j + (N + (1 : ℕ)).
  Uses library dvd_add, dvd_rfl.
  Lean, lines 36–39
  have hd : (j + 2) ∣ j + (N + 1) := by have : (j + 2) ∣ (k + 1).factorial := Nat.dvd_factorial (by omega) (by omega) have e : j + (N + 1) = (k + 1).factorial + (j + 2) := by rw [hN]; ring rw [e]; exact dvd_add this dvd_rfl
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 36–39 at 40da7e649495 ↗
  comp.hd.this have j + (2 : ℕ) ∣ (k + (1 : ℕ)).factorial
  Leaves j + (2 : ℕ) ∣ j + (N + (1 : ℕ)), with this : j + (2 : ℕ) ∣ (k + (1 : ℕ)).factorial.
  Uses library Nat.dvd_factorial.
  Lean, line 37
  have : (j + 2) ∣ (k + 1).factorial := Nat.dvd_factorial (by omega) (by omega)
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 37 at 40da7e649495 ↗
  comp.hd.e have j + (N + (1 : ℕ)) = (k + (1 : ℕ)).factorial + (j + (2 : ℕ))
  Leaves j + (2 : ℕ) ∣ j + (N + (1 : ℕ)), with e : j + (N + (1 : ℕ)) = (k + (1 : ℕ)).factorial + (j + (2 : ℕ)).
  Lean, line 38
  have e : j + (N + 1) = (k + 1).factorial + (j + 2) := by rw [hN]; ring
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 38 at 40da7e649495 ↗
2. comp.s2 case routine: omega
  Leaves False.
  Lean, line 41
  · omega
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 41 at 40da7e649495 ↗
3. comp.s3 case
  Leaves False.
  Lean, lines 42–43
  · have : 0 < (k + 1).factorial := Nat.factorial_pos _ rw [hN] at h; omega
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 42–43 at 40da7e649495 ↗
  comp.s3.this have (0 : ℕ) < (k + (1 : ℕ)).factorial
  Leaves False, with this : (0 : ℕ) < (k + (1 : ℕ)).factorial.
  Uses library Nat.factorial_pos.
  Lean, line 42
  · have : 0 < (k + 1).factorial := Nat.factorial_pos _
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 42 at 40da7e649495 ↗
hg have Summable fun (i : ℕ) => f (i + (N + (1 : ℕ)))
Leaves False, with hg : Summable fun (i : ℕ) => f (i + (N + (1 : ℕ))).
Uses library Summable, summable_nat_add_iff.
Lean, line 44
```
  have hg : Summable (fun i => f (i + (N + 1))) := (summable_nat_add_iff (N + 1)).mpr hs
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 44 at 40da7e649495 ↗
hg' have Summable fun (i : ℕ) => f (i + k + (N + (1 : ℕ)))
Leaves False, with hg' : Summable fun (i : ℕ) => f (i + k + (N + (1 : ℕ))).
Uses library Summable, add_assoc.
Lean, lines 45–47
```
  have hg' : Summable (fun i => f (i + k + (N + 1))) := by
    have := (summable_nat_add_iff k).mpr hg
    simpa [add_assoc] using this
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 45–47 at 40da7e649495 ↗
1. hg'.this have Summable fun (n : ℕ) => f (n + k + (N + (1 : ℕ)))
  Leaves Summable fun (i : ℕ) => f (i + k + (N + (1 : ℕ))), with this : Summable fun (n : ℕ) => f (n + k + (N + (1 : ℕ))).
  Uses library summable_nat_add_iff.
  Lean, line 46
  have := (summable_nat_add_iff k).mpr hg
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 46 at 40da7e649495 ↗
split1 have ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = ∑' (i : ℕ), f i
Leaves False, with split1 : ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = ∑' (i : ℕ), f i.
Uses library Summable.sum_add_tsum_nat_add.
Lean, line 48
```
  have split1 := Summable.sum_add_tsum_nat_add (N + 1) hs
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 48 at 40da7e649495 ↗
split2 have ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) + ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))) = ∑' (i : ℕ), f (i + (N + (1 : ℕ)))
Leaves False, with split2 : ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) + ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))) = ∑' (i : ℕ), f (i + (N + (1 : ℕ))).
Uses library Summable.sum_add_tsum_nat_add.
Lean, line 49
```
  have split2 := Summable.sum_add_tsum_nat_add k hg
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 49 at 40da7e649495 ↗
zero_part have ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) = (0 : ℝ)
Leaves False, with zero_part : ∑ i ∈ Finset.range k, f (i + (N + (1 : ℕ))) = (0 : ℝ).
Uses library Finset.range, Finset.sum_eq_zero.
Lean, lines 50–54
```
  have zero_part : ∑ i ∈ Finset.range k, f (i + (N + 1)) = 0 := by
    apply Finset.sum_eq_zero
    intro j hj
    have := comp j (Finset.mem_range.mp hj)
    simpa using this
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 50–54 at 40da7e649495 ↗
1. zero_part.this have f (j + k * (0 : ℕ) + (N + (1 : ℕ))) = (0 : ℝ)
  Leaves f (j + (N + (1 : ℕ))) = (0 : ℝ), with this : f (j + k * (0 : ℕ) + (N + (1 : ℕ))) = (0 : ℝ).
  Uses library Finset.mem_range.
  Lean, line 53
  have := comp j (Finset.mem_range.mp hj)
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 53 at 40da7e649495 ↗
split2' have ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = R
Leaves False, with split2' : ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = R.
Uses library zero_add.
Lean, lines 56–57
```
  have split2' : ∑' i, f (i + (N + 1)) = R := by
    rw [← split2, zero_part, zero_add]
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 56–57 at 40da7e649495 ↗
Rpos have (0 : ℝ) < R
Leaves False, with Rpos : (0 : ℝ) < R.
Uses library if_pos.
Lean, lines 59–63
```
  have Rpos : 0 < R := by
    obtain ⟨p, hp1, hp2⟩ := Nat.exists_infinite_primes (k + (N + 1))
    have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega
    refine hg'.tsum_pos (fun i => f_nonneg _) (p - (k + (N + 1))) ?_
    rw [hpi]; simp only [hf, if_pos hp2]; positivity
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 59–63 at 40da7e649495 ↗
1. Rpos.s1 obtain ∃ (p : ℕ), k + (N + (1 : ℕ)) ≤ p ∧ Nat.Prime p
  Leaves (0 : ℝ) < R, with p : ℕ, hp1 : k + (N + (1 : ℕ)) ≤ p, hp2 : Nat.Prime p.
  Uses library Nat.exists_infinite_primes.
  Lean, line 60
  obtain ⟨p, hp1, hp2⟩ := Nat.exists_infinite_primes (k + (N + 1))
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 60 at 40da7e649495 ↗
2. Rpos.hpi have p - (k + (N + (1 : ℕ))) + k + (N + (1 : ℕ)) = p routine: omega
  Leaves (0 : ℝ) < R, with hpi : p - (k + (N + (1 : ℕ))) + k + (N + (1 : ℕ)) = p.
  Lean, line 61
  have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 61 at 40da7e649495 ↗
geo have Summable fun (i : ℕ) => (1 / 2 : ℝ) ^ (i + k + (N + (1 : ℕ)))
Leaves False, with geo : Summable fun (i : ℕ) => (1 / 2 : ℝ) ^ (i + k + (N + (1 : ℕ))).
Uses library Summable, add_assoc.
Lean, lines 65–68
```
  have geo : Summable (fun i : ℕ => (1 / 2 : ℝ) ^ (i + k + (N + 1))) := by
    have := (summable_nat_add_iff (k + (N + 1))).mpr
      (summable_geometric_of_lt_one (by norm_num : (0:ℝ) ≤ 1 / 2) (by norm_num))
    simpa [add_assoc] using this
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 65–68 at 40da7e649495 ↗
1. geo.this have Summable fun (n : ℕ) => (1 / 2 : ℝ) ^ (n + (k + (N + (1 : ℕ))))
  Leaves Summable fun (i : ℕ) => (1 / 2 : ℝ) ^ (i + k + (N + (1 : ℕ))), with this : Summable fun (n : ℕ) => (1 / 2 : ℝ) ^ (n + (k + (N + (1 : ℕ)))).
  Uses library summable_nat_add_iff, summable_geometric_of_lt_one.
  Lean, lines 66–67
  have := (summable_nat_add_iff (k + (N + 1))).mpr (summable_geometric_of_lt_one (by norm_num : (0:ℝ) ≤ 1 / 2) (by norm_num))
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 66–67 at 40da7e649495 ↗
Rle have R ≤ (1 / 2 : ℝ) ^ (k + (N + (1 : ℕ))) * (2 : ℝ)
Leaves False, with Rle : R ≤ (1 / 2 : ℝ) ^ (k + (N + (1 : ℕ))) * (2 : ℝ).
Lean, lines 69–74
```
  have Rle : R ≤ (1 / 2 : ℝ) ^ (k + (N + 1)) * 2 := by
    calc R ≤ ∑' i : ℕ, (1 / 2 : ℝ) ^ (i + k + (N + 1)) :=
          Summable.tsum_le_tsum (fun i => f_le _) hg' geo
      _ = (1 / 2 : ℝ) ^ (k + (N + 1)) * 2 := by
          simp_rw [add_assoc, pow_add]
          rw [tsum_mul_right, tsum_geometric_two, mul_comm]
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 69–74 at 40da7e649495 ↗
1. Rle.s1 calc R ≤ ∑' (i : ℕ), (1 / 2 : ℝ) ^ (i + k + (N + (1 : ℕ)))
  Closes the goal.
  Uses library Summable.tsum_le_tsum.
  Lean, lines 70–71
  calc R ≤ ∑' i : ℕ, (1 / 2 : ℝ) ^ (i + k + (N + 1)) := Summable.tsum_le_tsum (fun i => f_le _) hg' geo
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 70–71 at 40da7e649495 ↗
2. Rle.s2 calc
  Closes the goal.
  Uses library add_assoc, pow_add, tsum_mul_right, tsum_geometric_two, mul_comm.
  Lean, lines 72–74
  _ = (1 / 2 : ℝ) ^ (k + (N + 1)) * 2 := by simp_rw [add_assoc, pow_add] rw [tsum_mul_right, tsum_geometric_two, mul_comm]
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 72–74 at 40da7e649495 ↗
key have (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = (1 / 2 : ℝ) ^ k
Leaves False, with key : (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = (1 / 2 : ℝ) ^ k.
Lean, lines 75–80
```
  have key : (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + 1)) * 2) = (1 / 2) ^ k := by
    have h1 : (2 : ℝ) ^ N * (1 / 2) ^ N = 1 := by rw [← mul_pow]; norm_num
    calc (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + 1)) * 2)
        = (1 / 2) ^ k * ((2 : ℝ) ^ N * (1 / 2) ^ N) * ((1 / 2) * 2) := by
          rw [pow_add, pow_succ]; ring
      _ = (1 / 2) ^ k := by rw [h1]; norm_num
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 75–80 at 40da7e649495 ↗
1. key.h1 have (2 : ℝ) ^ N * (1 / 2 : ℝ) ^ N = (1 : ℝ)
  Leaves (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = (1 / 2 : ℝ) ^ k, with h1 : (2 : ℝ) ^ N * (1 / 2 : ℝ) ^ N = (1 : ℝ).
  Uses library mul_pow.
  Lean, line 76
  have h1 : (2 : ℝ) ^ N * (1 / 2) ^ N = 1 := by rw [← mul_pow]; norm_num
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 76 at 40da7e649495 ↗
2. key.s2 calc (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = (1 / 2 : ℝ) ^ k * ((2 : ℝ) ^ N * (1 / 2 : ℝ) ^ N) * ((1 / 2 : ℝ) * (2 : ℝ))
  Closes the goal.
  Uses library pow_add, pow_succ.
  Lean, lines 77–79
  calc (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + 1)) * 2) = (1 / 2) ^ k * ((2 : ℝ) ^ N * (1 / 2) ^ N) * ((1 / 2) * 2) := by rw [pow_add, pow_succ]; ring
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 77–79 at 40da7e649495 ↗
3. key.s3 calc
  Closes the goal.
  Lean, line 80
  _ = (1 / 2) ^ k := by rw [h1]; norm_num
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 80 at 40da7e649495 ↗
hZ' have (2 : ℝ) ^ N * ∑ i ∈ Finset.range (N + (1 : ℕ)), f i = (↑Z : ℝ)
Leaves False, with hZ' : (2 : ℝ) ^ N * ∑ i ∈ Finset.range (N + (1 : ℕ)), f i = (↑Z : ℝ).
Uses library Finset.range, Finset.mul_sum, Finset.sum_congr, rfl.
Lean, lines 83–93
```
  have hZ' : (2 : ℝ) ^ N * ∑ i ∈ Finset.range (N + 1), f i = (Z : ℝ) := by
    rw [hZ, Finset.mul_sum]; push_cast
    apply Finset.sum_congr rfl
    intro i hi
    have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
    simp only [hf]
    split_ifs
    · have e : (2 : ℝ) ^ N = 2 ^ (N - i) * 2 ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow]; norm_num
    · simp
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 83–93 at 40da7e649495 ↗
1. hZ'.hi' have i ≤ N
  Leaves (2 : ℝ) ^ N * f i = if Nat.Prime i then (2 : ℝ) ^ (N - i) else (0 : ℝ), with hi' : i ≤ N.
  Uses library Nat.lt_succ_iff, Finset.mem_range.
  Lean, line 87
  have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 87 at 40da7e649495 ↗
2. hZ'.s2 case
  Leaves (2 : ℝ) ^ N * (1 / 2 : ℝ) ^ i = (2 : ℝ) ^ (N - i).
  Uses library mul_assoc, mul_pow.
  Lean, lines 90–92
  · have e : (2 : ℝ) ^ N = 2 ^ (N - i) * 2 ^ i := by rw [← pow_add, Nat.sub_add_cancel hi'] rw [e, mul_assoc, ← mul_pow]; norm_num
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 90–92 at 40da7e649495 ↗
  hZ'.s2.e have (2 : ℝ) ^ N = (2 : ℝ) ^ (N - i) * (2 : ℝ) ^ i
  Leaves (2 : ℝ) ^ N * (1 / 2 : ℝ) ^ i = (2 : ℝ) ^ (N - i), with e : (2 : ℝ) ^ N = (2 : ℝ) ^ (N - i) * (2 : ℝ) ^ i.
  Uses library pow_add, Nat.sub_add_cancel.
  Lean, lines 90–91
  · have e : (2 : ℝ) ^ N = 2 ^ (N - i) * 2 ^ i := by rw [← pow_add, Nat.sub_add_cancel hi']
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 90–91 at 40da7e649495 ↗
3. hZ'.s3 case routine: simp
  Leaves (2 : ℝ) ^ N * (0 : ℝ) = (0 : ℝ).
  Lean, line 93
  · simp
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 93 at 40da7e649495 ↗
hqk have (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ)
Leaves False, with hqk : (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ).
Uses library Rat.mul_den_eq_num.
Lean, line 94
```
  have hqk : (q : ℝ) * k = q.num := by exact_mod_cast Rat.mul_den_eq_num q
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 94 at 40da7e649495 ↗
hx have (↑q : ℝ) = ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + R
Leaves False, with hx : (↑q : ℝ) = ∑ i ∈ Finset.range (N + (1 : ℕ)), f i + R.
Uses library Finset.range.
Lean, lines 96–97
```
  have hx : (q : ℝ) = ∑ i ∈ Finset.range (N + 1), f i + R := by
    rw [hq, ← split1, split2']
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 96–97 at 40da7e649495 ↗
hm have (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((2 : ℝ) ^ N * R)
Leaves False, with hm : (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((2 : ℝ) ^ N * R).
Lean, lines 98–100
```
  have hm : ((2 ^ N * q.num - k * Z : ℤ) : ℝ) = (k : ℝ) * ((2 : ℝ) ^ N * R) := by
    push_cast
    rw [← hqk, hx, ← hZ']; ring
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 98–100 at 40da7e649495 ↗
mpos have (0 : ℝ) < (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ)
Leaves False, with mpos : (0 : ℝ) < (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ).
Lean, lines 101–103
```
  have mpos : (0 : ℝ) < ((2 ^ N * q.num - k * Z : ℤ) : ℝ) := by
    rw [hm]; have : (0 : ℝ) < k := by exact_mod_cast kpos
    positivity
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 101–103 at 40da7e649495 ↗
1. mpos.this have (0 : ℝ) < (↑k : ℝ)
  Leaves (0 : ℝ) < (↑k : ℝ) * ((2 : ℝ) ^ N * R), with this : (0 : ℝ) < (↑k : ℝ).
  Lean, line 102
  rw [hm]; have : (0 : ℝ) < k := by exact_mod_cast kpos
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 102 at 40da7e649495 ↗
mlt have (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ)
Leaves False, with mlt : (↑((2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ).
Lean, lines 104–112
```
  have mlt : ((2 ^ N * q.num - k * Z : ℤ) : ℝ) < 1 := by
    rw [hm]
    have h2 : (2 : ℝ) ^ N * R ≤ (1 / 2) ^ k := by
      rw [← key]; exact mul_le_mul_of_nonneg_left Rle (by positivity)
    have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hk0 : (0 : ℝ) ≤ k := by positivity
    calc (k : ℝ) * ((2 : ℝ) ^ N * R) ≤ k * (1 / 2) ^ k := mul_le_mul_of_nonneg_left h2 hk0
      _ = k / 2 ^ k := by rw [one_div_pow, mul_one_div]
      _ < 1 := by rw [div_lt_one (by positivity)]; exact hk2
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 104–112 at 40da7e649495 ↗
1. mlt.h2 have (2 : ℝ) ^ N * R ≤ (1 / 2 : ℝ) ^ k
  Leaves (↑k : ℝ) * ((2 : ℝ) ^ N * R) < (1 : ℝ), with h2 : (2 : ℝ) ^ N * R ≤ (1 / 2 : ℝ) ^ k.
  Uses library mul_le_mul_of_nonneg_left.
  Lean, lines 106–107
  have h2 : (2 : ℝ) ^ N * R ≤ (1 / 2) ^ k := by rw [← key]; exact mul_le_mul_of_nonneg_left Rle (by positivity)
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, lines 106–107 at 40da7e649495 ↗
2. mlt.hk2 have (↑k : ℝ) < (2 : ℝ) ^ k
  Leaves (↑k : ℝ) * ((2 : ℝ) ^ N * R) < (1 : ℝ), with hk2 : (↑k : ℝ) < (2 : ℝ) ^ k.
  Uses library Nat.lt_two_pow_self.
  Lean, line 108
  have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 108 at 40da7e649495 ↗
3. mlt.hk0 have (0 : ℝ) ≤ (↑k : ℝ) routine: positivity
  Leaves (↑k : ℝ) * ((2 : ℝ) ^ N * R) < (1 : ℝ), with hk0 : (0 : ℝ) ≤ (↑k : ℝ).
  Lean, line 109
  have hk0 : (0 : ℝ) ≤ k := by positivity
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 109 at 40da7e649495 ↗
4. mlt.s4 calc (↑k : ℝ) * ((2 : ℝ) ^ N * R) ≤ (↑k : ℝ) * (1 / 2 : ℝ) ^ k
  Closes the goal.
  Uses library mul_le_mul_of_nonneg_left.
  Lean, line 110
  calc (k : ℝ) * ((2 : ℝ) ^ N * R) ≤ k * (1 / 2) ^ k := mul_le_mul_of_nonneg_left h2 hk0
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 110 at 40da7e649495 ↗
5. mlt.s5 calc
  Closes the goal.
  Uses library one_div_pow, mul_one_div.
  Lean, line 111
  _ = k / 2 ^ k := by rw [one_div_pow, mul_one_div]
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 111 at 40da7e649495 ↗
6. mlt.s6 calc
  Closes the goal.
  Uses library div_lt_one.
  Lean, line 112
  _ < 1 := by rw [div_lt_one (by positivity)]; exact hk2
  targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 112 at 40da7e649495 ↗
i1 have (0 : ℤ) < (2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)
Leaves False, with i1 : (0 : ℤ) < (2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ).
Lean, line 113
```
  have i1 : (0 : ℤ) < 2 ^ N * q.num - k * Z := by exact_mod_cast mpos
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 113 at 40da7e649495 ↗
i2 have (2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ)
Leaves False, with i2 : (2 : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ).
Lean, line 114
```
  have i2 : 2 ^ N * q.num - k * Z < (1 : ℤ) := by exact_mod_cast mlt
```
targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, line 114 at 40da7e649495 ↗

The proof in Lean (Proof.lean)

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

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-69/nodes/variant-09e95e7a/Proof.lean, sha256 acdf97b1e300.

import Mathlib
import Nodes.«variant-09e95e7a».Context

/-! A related variant of Erdős problem 69 (D-30, relation `related`): the binary number whose
n-th digit is 1 exactly when n is prime, `∑_{p prime} 2^{-p}`, is irrational.

Why it sits beside erdos-69: the root's standing decomposition (erdos-69--h2-v2 and below) turns
rationality of `∑ ω(n)/2^n` into "b times every tail `∑_{j≥1} ω(N+j)/2^j` is an integer" and is
blocked on controlling ω on a window of consecutive integers. For the prime indicator the same
tail argument closes, because the window is controllable: `(k+1)! + 2, …, (k+1)! + k + 1` are
all composite, so the tail after `N = (k+1)! + 1` lies strictly between 0 and `2^{-k}`. This
node is a worked, gate-checked instance of the method, not progress on the root. -/

theorem Opn.erdos_69_prime_indicator :
    Irrational (∑' n : ℕ, if n.Prime then (1 / 2 : ℝ) ^ n else 0) := by
  set f : ℕ → ℝ := fun n => if n.Prime then (1 / 2 : ℝ) ^ n else 0 with hf
  have f_nonneg : ∀ n, 0 ≤ f n := fun n => by
    simp only [hf]; split_ifs <;> positivity
  have f_le : ∀ n, f n ≤ (1 / 2 : ℝ) ^ n := fun n => by
    simp only [hf]; split_ifs
    · exact le_rfl
    · positivity
  have hs : Summable f :=
    Summable.of_nonneg_of_le f_nonneg f_le
      (summable_geometric_of_lt_one (by norm_num) (by norm_num))
  rintro ⟨q, hq⟩
  set k := q.den with hk
  have kpos : 0 < k := q.den_pos
  set N := (k + 1).factorial + 1 with hN
  -- the k integers after N are composite
  have comp : ∀ j, j < k → f (j + k * 0 + (N + 1)) = 0 := by
    intro j hj
    simp only [hf, mul_zero, add_zero]
    rw [if_neg]
    intro hp
    have hd : (j + 2) ∣ j + (N + 1) := by
      have : (j + 2) ∣ (k + 1).factorial := Nat.dvd_factorial (by omega) (by omega)
      have e : j + (N + 1) = (k + 1).factorial + (j + 2) := by rw [hN]; ring
      rw [e]; exact dvd_add this dvd_rfl
    rcases hp.eq_one_or_self_of_dvd _ hd with h | h
    · omega
    · have : 0 < (k + 1).factorial := Nat.factorial_pos _
      rw [hN] at h; omega
  have hg : Summable (fun i => f (i + (N + 1))) := (summable_nat_add_iff (N + 1)).mpr hs
  have hg' : Summable (fun i => f (i + k + (N + 1))) := by
    have := (summable_nat_add_iff k).mpr hg
    simpa [add_assoc] using this
  have split1 := Summable.sum_add_tsum_nat_add (N + 1) hs
  have split2 := Summable.sum_add_tsum_nat_add k hg
  have zero_part : ∑ i ∈ Finset.range k, f (i + (N + 1)) = 0 := by
    apply Finset.sum_eq_zero
    intro j hj
    have := comp j (Finset.mem_range.mp hj)
    simpa using this
  set R := ∑' i, f (i + k + (N + 1)) with hR
  have split2' : ∑' i, f (i + (N + 1)) = R := by
    rw [← split2, zero_part, zero_add]
  -- R is positive
  have Rpos : 0 < R := by
    obtain ⟨p, hp1, hp2⟩ := Nat.exists_infinite_primes (k + (N + 1))
    have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega
    refine hg'.tsum_pos (fun i => f_nonneg _) (p - (k + (N + 1))) ?_
    rw [hpi]; simp only [hf, if_pos hp2]; positivity
  -- R is small
  have geo : Summable (fun i : ℕ => (1 / 2 : ℝ) ^ (i + k + (N + 1))) := by
    have := (summable_nat_add_iff (k + (N + 1))).mpr
      (summable_geometric_of_lt_one (by norm_num : (0:ℝ) ≤ 1 / 2) (by norm_num))
    simpa [add_assoc] using this
  have Rle : R ≤ (1 / 2 : ℝ) ^ (k + (N + 1)) * 2 := by
    calc R ≤ ∑' i : ℕ, (1 / 2 : ℝ) ^ (i + k + (N + 1)) :=
          Summable.tsum_le_tsum (fun i => f_le _) hg' geo
      _ = (1 / 2 : ℝ) ^ (k + (N + 1)) * 2 := by
          simp_rw [add_assoc, pow_add]
          rw [tsum_mul_right, tsum_geometric_two, mul_comm]
  have key : (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + 1)) * 2) = (1 / 2) ^ k := by
    have h1 : (2 : ℝ) ^ N * (1 / 2) ^ N = 1 := by rw [← mul_pow]; norm_num
    calc (2 : ℝ) ^ N * ((1 / 2 : ℝ) ^ (k + (N + 1)) * 2)
        = (1 / 2) ^ k * ((2 : ℝ) ^ N * (1 / 2) ^ N) * ((1 / 2) * 2) := by
          rw [pow_add, pow_succ]; ring
      _ = (1 / 2) ^ k := by rw [h1]; norm_num
  -- the finite part times 2^N is an integer
  set Z : ℕ := ∑ i ∈ Finset.range (N + 1), if i.Prime then 2 ^ (N - i) else 0 with hZ
  have hZ' : (2 : ℝ) ^ N * ∑ i ∈ Finset.range (N + 1), f i = (Z : ℝ) := by
    rw [hZ, Finset.mul_sum]; push_cast
    apply Finset.sum_congr rfl
    intro i hi
    have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)
    simp only [hf]
    split_ifs
    · have e : (2 : ℝ) ^ N = 2 ^ (N - i) * 2 ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow]; norm_num
    · simp
  have hqk : (q : ℝ) * k = q.num := by exact_mod_cast Rat.mul_den_eq_num q
  -- m := k * 2^N * R is an integer
  have hx : (q : ℝ) = ∑ i ∈ Finset.range (N + 1), f i + R := by
    rw [hq, ← split1, split2']
  have hm : ((2 ^ N * q.num - k * Z : ℤ) : ℝ) = (k : ℝ) * ((2 : ℝ) ^ N * R) := by
    push_cast
    rw [← hqk, hx, ← hZ']; ring
  have mpos : (0 : ℝ) < ((2 ^ N * q.num - k * Z : ℤ) : ℝ) := by
    rw [hm]; have : (0 : ℝ) < k := by exact_mod_cast kpos
    positivity
  have mlt : ((2 ^ N * q.num - k * Z : ℤ) : ℝ) < 1 := by
    rw [hm]
    have h2 : (2 : ℝ) ^ N * R ≤ (1 / 2) ^ k := by
      rw [← key]; exact mul_le_mul_of_nonneg_left Rle (by positivity)
    have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hk0 : (0 : ℝ) ≤ k := by positivity
    calc (k : ℝ) * ((2 : ℝ) ^ N * R) ≤ k * (1 / 2) ^ k := mul_le_mul_of_nonneg_left h2 hk0
      _ = k / 2 ^ k := by rw [one_div_pow, mul_one_div]
      _ < 1 := by rw [div_lt_one (by positivity)]; exact hk2
  have i1 : (0 : ℤ) < 2 ^ N * q.num - k * Z := by exact_mod_cast mpos
  have i2 : 2 ^ N * q.num - k * Z < (1 : ℤ) := by exact_mod_cast mlt
  omega

What is known

Work on it

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (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-09e95e7a».Context

/-! A related variant of Erdős problem 69 (D-30, relation `related`): the binary number whose
n-th digit is 1 exactly when n is prime, `∑_{p prime} 2^{-p}`, is irrational.

Why it sits beside erdos-69: the root's standing decomposition (erdos-69--h2-v2 and below) turns
rationality of `∑ ω(n)/2^n` into "b times every tail `∑_{j≥1} ω(N+j)/2^j` is an integer" and is
blocked on controlling ω on a window of consecutive integers. For the prime indicator the same
tail argument closes, because the window is controllable: `(k+1)! + 2, …, (k+1)! + k + 1` are
all composite, so the tail after `N = (k+1)! + 1` lies strictly between 0 and `2^{-k}`. This
node is a worked, gate-checked instance of the method, not progress on the root. -/

theorem Opn.erdos_69_prime_indicator :
    Irrational (∑' n : ℕ, if n.Prime then (1 / 2 : ℝ) ^ n else 0) := by
  sorry

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \sum_{n=0}^{\infty}\bigl[n\ \text{prime}\bigr]\Bigl(\frac{1}{2}\Bigr)^{n} \notin\mathbb{Q}$

Rendered from gloss/66af1da98650….md · Improve these words →

Rendered from targets/erdos-69/nodes/variant-09e95e7a/Statement.lean. Origin: variant (related).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000224.json, merge commit 40da7e649495.

Verdict pass, from attestations/000224.json.

Submitter: mcp-e69-sep27
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

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/000224.json, merge commit 40da7e649495.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/variant-09e95e7a/Witness.lean, sha256 32191282b59e.

/-! Non-vacuity witness (D-4 step 7): the statement has no hypotheses, so the expected
witness type is `True`. -/

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 →

How to read this page

How to read a statement’s page →

Explainer

Idea and method

Bounds on the terms and convergence

A block of $k$ vanishing terms

Splitting the series

The tail is positive

The tail is small

The head is an integer after scaling

An integer strictly between $0$ and $1$

Idea and method

Bounds on the terms and convergence (f_nonneg f_le f_le.s1 f_le.s2 hs)

A block of $k$ vanishing terms (kpos comp comp.hd comp.hd.this comp.hd.e comp.s2 comp.s3 comp.s3.this)

Splitting the series (hg hg' hg'.this split1 split2 zero_part zero_part.this split2')

The tail is positive (Rpos Rpos.s1 Rpos.hpi)

The tail is small (geo geo.this Rle Rle.s1 Rle.s2 key key.h1 key.s2 key.s3)

The head is an integer after scaling (hZ' hZ'.hi' hZ'.s2 hZ'.s2.e hZ'.s3)

An integer strictly between $0$ and $1$ (hqk hx hm mpos mpos.this mlt mlt.h2 mlt.hk2 mlt.hk0 mlt.s4 mlt.s5 mlt.s6 i1 i2)

How it was proved

What is known

Work on it

Record