Open Proof Network

Problems / erdos-69 / variant-f592e3ab

Irrationality of the prime indicator in any base

variant-f592e3ab

proved

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

$\displaystyle \forall b\in\mathbb{N},\ b\ge 2:\quad \sum_{p\ \text{prime}}\frac{1}{b^{p}} \notin\mathbb{Q}$

For every natural base b ≥ 2, the sum over the primes p of 1/b^p, in ℝ, 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_primes_any_base :
    ∀ b : ℕ, 2 ≤ b → Irrational (∑' p : Nat.Primes, (1 : ℝ) / (b : ℝ) ^ (p : ℕ)) := 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 →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000300, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000300.json, merge commit dc94c2f71b52.

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.

  1. hb0 have (2 : ℝ) ≤ (↑b : ℝ)

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with hb0 : (2 : ℝ) ≤ (↑b : ℝ).

    Lean, line 20
      have hb0 : (2 : ℝ) ≤ (b : ℝ) := by exact_mod_cast hb

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 20 at dc94c2f71b52 ↗

  2. bpos have (0 : ℝ) < (↑b : ℝ) routine: linarith

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with bpos : (0 : ℝ) < (↑b : ℝ).

    Lean, line 21
      have bpos : (0 : ℝ) < b := by linarith

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 21 at dc94c2f71b52 ↗

  3. s3 obtain ∃ (r : ℝ), r = (1 : ℝ) / (↑b : ℝ)

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with r : ℝ, hr : r = (1 : ℝ) / (↑b : ℝ).

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

    Lean, line 22
      obtain ⟨r, hr⟩ : ∃ r : ℝ, r = 1 / (b : ℝ) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 22 at dc94c2f71b52 ↗

  4. r0 have (0 : ℝ) < r

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with r0 : (0 : ℝ) < r.

    Uses library one_div_pos.

    Lean, line 23
      have r0 : 0 < r := by rw [hr]; exact one_div_pos.mpr bpos

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 23 at dc94c2f71b52 ↗

  5. r2 have r ≤ (1 / 2 : ℝ)

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with r2 : r ≤ (1 / 2 : ℝ).

    Uses library one_div_le_one_div_of_le.

    Lean, line 24
      have r2 : r ≤ 1 / 2 := by rw [hr]; exact one_div_le_one_div_of_le (by norm_num) hb0

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 24 at dc94c2f71b52 ↗

  6. rb have r * (↑b : ℝ) = (1 : ℝ)

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with rb : r * (↑b : ℝ) = (1 : ℝ).

    Uses library one_div, inv_mul_cancel₀.

    Lean, line 25
      have rb : r * (b : ℝ) = 1 := by rw [hr, one_div, inv_mul_cancel₀ bpos.ne']

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 25 at dc94c2f71b52 ↗

  7. s7 obtain ∃ (f : ℕ → ℝ), f = fun (n : ℕ) => if Nat.Prime n then r ^ n else (0 : ℝ)

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with f : ℕ → ℝ, hf : f = fun (n : ℕ) => if Nat.Prime n then r ^ n else (0 : ℝ).

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

    Lean, line 26
      obtain ⟨f, hf⟩ : ∃ f : ℕ → ℝ, f = fun n => if n.Prime then r ^ n else 0 := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 26 at dc94c2f71b52 ↗

  8. hconv have ∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ) = ∑' (n : ℕ), f n

    Leaves Irrational (∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ)), with hconv : ∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ) = ∑' (n : ℕ), f n.

    Uses library Nat.Primes The type of prime numbers , Set.indicator_apply, Set.mem_ofPred_eq, one_div_pow.

    Lean, lines 27–31
      have hconv : ∑' p : Nat.Primes, (1 : ℝ) / (b : ℝ) ^ (p : ℕ) = ∑' n : ℕ, f n := by
    have h := tsum_subtype {p : ℕ | p.Prime} (fun n : ℕ => (1 : ℝ) / (b : ℝ) ^ n)
    refine h.trans ?_
    congr 1; funext n
    simp only [Set.indicator_apply, Set.mem_ofPred_eq, hf, hr, one_div_pow]

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 27–31 at dc94c2f71b52 ↗

    1. hconv.h have ∑' (x : (↑{p : ℕ | Nat.Prime p} : Type)), (1 : ℝ) / (↑b : ℝ) ^ (↑x : ℕ) = ∑' (x : ℕ), {p : ℕ | Nat.Prime p}.indicator (fun (n : ℕ) => (1 : ℝ) / (↑b : ℝ) ^ n) x

      Leaves ∑' (p : Nat.Primes), (1 : ℝ) / (↑b : ℝ) ^ (↑p : ℕ) = ∑' (n : ℕ), f n, with h : ∑' (x : (↑{p : ℕ | Nat.Prime p} : Type)), (1 : ℝ) / (↑b : ℝ) ^ (↑x : ℕ) = ∑' (x : ℕ), {p : ℕ | Nat.Prime p}.indicator (fun (n : ℕ) => (1 : ℝ) / (↑b : ℝ) ^ n) x.

      Uses library tsum_subtype.

      Lean, line 28
          have h := tsum_subtype {p : ℕ | p.Prime} (fun n : ℕ => (1 : ℝ) / (b : ℝ) ^ n)

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 28 at dc94c2f71b52 ↗

  9. f_nonneg have ∀ (n : ℕ), (0 : ℝ) ≤ f n

    Leaves Irrational (∑' (n : ℕ), f n), with f_nonneg : ∀ (n : ℕ), (0 : ℝ) ≤ f n.

    Lean, lines 33–36
      have f_nonneg : ∀ n, 0 ≤ f n := fun n => by
    simp only [hf]; split_ifs
    · exact pow_nonneg r0.le n
    · exact le_rfl

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 33–36 at dc94c2f71b52 ↗

    1. f_nonneg.s1 case

      Leaves (0 : ℝ) ≤ r ^ n.

      Uses library pow_nonneg.

      Lean, line 35
          · exact pow_nonneg r0.le n

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 35 at dc94c2f71b52 ↗

    2. f_nonneg.s2 case

      Leaves (0 : ℝ) ≤ (0 : ℝ).

      Uses library le_rfl A version of le_refl where the argument is implicit .

      Lean, line 36
          · exact le_rfl

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 36 at dc94c2f71b52 ↗

  10. f_le have ∀ (n : ℕ), f n ≤ r ^ n

    Leaves Irrational (∑' (n : ℕ), f n), with f_le : ∀ (n : ℕ), f n ≤ r ^ n.

    Lean, lines 37–40
      have f_le : ∀ n, f n ≤ r ^ n := fun n => by
    simp only [hf]; split_ifs
    · exact le_rfl
    · exact pow_nonneg r0.le n

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 37–40 at dc94c2f71b52 ↗

    1. f_le.s1 case

      Leaves r ^ n ≤ r ^ n.

      Uses library le_rfl A version of le_refl where the argument is implicit .

      Lean, line 39
          · exact le_rfl

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 39 at dc94c2f71b52 ↗

    2. f_le.s2 case

      Leaves (0 : ℝ) ≤ r ^ n.

      Uses library pow_nonneg.

      Lean, line 40
          · exact pow_nonneg r0.le n

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 40 at dc94c2f71b52 ↗

  11. hs have Summable f

    Leaves Irrational (∑' (n : ℕ), f n), with hs : Summable f.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , Summable.of_nonneg_of_le Comparison test of convergence of series of non-negative real numbers. , summable_geometric_of_lt_one.

    Lean, lines 41–43
      have hs : Summable f :=
    Summable.of_nonneg_of_le f_nonneg f_le
      (summable_geometric_of_lt_one r0.le (by linarith))

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 41–43 at dc94c2f71b52 ↗

  12. s12 obtain ∃ (k : ℕ), k = q.den

    Leaves False, with k : ℕ, hk : k = q.den.

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

    Lean, line 45
      obtain ⟨k, hk⟩ : ∃ k, k = q.den := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 45 at dc94c2f71b52 ↗

  13. kpos have (0 : ℕ) < k

    Leaves False, with kpos : (0 : ℕ) < k.

    Lean, line 46
      have kpos : 0 < k := by rw [hk]; exact q.den_pos

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 46 at dc94c2f71b52 ↗

  14. s14 obtain ∃ (N : ℕ), N = (k + (1 : ℕ)).factorial + (1 : ℕ)

    Leaves False, with N : ℕ, hN : N = (k + (1 : ℕ)).factorial + (1 : ℕ).

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

    Lean, line 47
      obtain ⟨N, hN⟩ : ∃ N, N = (k + 1).factorial + 1 := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 47 at dc94c2f71b52 ↗

  15. comp have ∀ j < k, f (j + (N + (1 : ℕ))) = (0 : ℝ)

    Leaves False, with comp : ∀ j < k, f (j + (N + (1 : ℕ))) = (0 : ℝ).

    Uses library if_neg.

    Lean, lines 48–60
      have comp : ∀ j, j < k → f (j + (N + 1)) = 0 := by
    intro j hj
    simp only [hf]
    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-f592e3ab/Proof.lean, lines 48–60 at dc94c2f71b52 ↗

    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 53–56
          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-f592e3ab/Proof.lean, lines 53–56 at dc94c2f71b52 ↗

      1. 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 54
              have : (j + 2) ∣ (k + 1).factorial := Nat.dvd_factorial (by omega) (by omega)

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 54 at dc94c2f71b52 ↗

      2. 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 55
              have e : j + (N + 1) = (k + 1).factorial + (j + 2) := by rw [hN]; ring

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 55 at dc94c2f71b52 ↗

    2. comp.s2 case routine: omega

      Leaves False.

      Lean, line 58
          · omega

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 58 at dc94c2f71b52 ↗

    3. comp.s3 case

      Leaves False.

      Lean, lines 59–60
          · have : 0 < (k + 1).factorial := Nat.factorial_pos _
      rw [hN] at h; omega

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 59–60 at dc94c2f71b52 ↗

      1. comp.s3.this have (0 : ℕ) < (k + (1 : ℕ)).factorial

        Leaves False, with this : (0 : ℕ) < (k + (1 : ℕ)).factorial.

        Uses library Nat.factorial_pos.

        Lean, line 59
            · have : 0 < (k + 1).factorial := Nat.factorial_pos _

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 59 at dc94c2f71b52 ↗

  16. hg have Summable fun (i : ℕ) => f (i + (N + (1 : ℕ)))

    Leaves False, with hg : Summable fun (i : ℕ) => f (i + (N + (1 : ℕ))).

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_nat_add_iff.

    Lean, line 61
      have hg : Summable (fun i => f (i + (N + 1))) := (summable_nat_add_iff (N + 1)).mpr hs

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 61 at dc94c2f71b52 ↗

  17. 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 Summable f means that f has some (infinite) sum with respect to L. , add_assoc.

    Lean, lines 62–64
      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-f592e3ab/Proof.lean, lines 62–64 at dc94c2f71b52 ↗

    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 63
          have := (summable_nat_add_iff k).mpr hg

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 63 at dc94c2f71b52 ↗

  18. 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 65
      have split1 := Summable.sum_add_tsum_nat_add (N + 1) hs

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 65 at dc94c2f71b52 ↗

  19. 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 66
      have split2 := Summable.sum_add_tsum_nat_add k hg

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 66 at dc94c2f71b52 ↗

  20. 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 range n is the set of natural numbers less than n. , Finset.sum_eq_zero, Finset.mem_range.

    Lean, lines 67–70
      have zero_part : ∑ i ∈ Finset.range k, f (i + (N + 1)) = 0 := by
    apply Finset.sum_eq_zero
    intro j hj
    exact comp j (Finset.mem_range.mp hj)

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 67–70 at dc94c2f71b52 ↗

  21. s21 obtain ∃ (R : ℝ), R = ∑' (i : ℕ), f (i + k + (N + (1 : ℕ)))

    Leaves False, with R : ℝ, hR : R = ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))).

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

    Lean, line 71
      obtain ⟨R, hR⟩ : ∃ R, R = ∑' i, f (i + k + (N + 1)) := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 71 at dc94c2f71b52 ↗

  22. split2' have ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = R

    Leaves False, with split2' : ∑' (i : ℕ), f (i + (N + (1 : ℕ))) = R.

    Uses library zero_add.

    Lean, lines 72–73
      have split2' : ∑' i, f (i + (N + 1)) = R := by
    rw [← split2, zero_part, zero_add, hR]

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 72–73 at dc94c2f71b52 ↗

  23. Rpos have (0 : ℝ) < R

    Leaves False, with Rpos : (0 : ℝ) < R.

    Uses library if_pos, pow_pos.

    Lean, lines 74–79
      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
    rw [hR]
    refine hg'.tsum_pos (fun i => f_nonneg _) (p - (k + (N + 1))) ?_
    rw [hpi]; simp only [hf, if_pos hp2]; exact pow_pos r0 p

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 74–79 at dc94c2f71b52 ↗

    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 Euclid's theorem on the infinitude of primes. .

      Lean, line 75
          obtain ⟨p, hp1, hp2⟩ := Nat.exists_infinite_primes (k + (N + 1))

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 75 at dc94c2f71b52 ↗

    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 76
          have hpi : p - (k + (N + 1)) + k + (N + 1) = p := by omega

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 76 at dc94c2f71b52 ↗

  24. geo have Summable fun (i : ℕ) => r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

    Leaves False, with geo : Summable fun (i : ℕ) => r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i.

    Uses library Summable Summable f means that f has some (infinite) sum with respect to L. , summable_geometric_two.

    Lean, lines 80–81
      have geo : Summable (fun i : ℕ => r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i) :=
    summable_geometric_two.mul_left _

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 80–81 at dc94c2f71b52 ↗

  25. term_le have ∀ (i : ℕ), f (i + k + (N + (1 : ℕ))) ≤ r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

    Leaves False, with term_le : ∀ (i : ℕ), f (i + k + (N + (1 : ℕ))) ≤ r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i.

    Lean, lines 82–87
      have term_le : ∀ i, f (i + k + (N + 1)) ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i := by
    intro i
    calc f (i + k + (N + 1)) ≤ r ^ (i + k + (N + 1)) := f_le _
      _ = r ^ (k + (N + 1)) * r ^ i := by ring
      _ ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ r0.le r2 i) (pow_nonneg r0.le _)

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 82–87 at dc94c2f71b52 ↗

    1. term_le.s1 calc f (i + k + (N + (1 : ℕ))) ≤ r ^ (i + k + (N + (1 : ℕ)))

      Closes the goal.

      Lean, line 84
          calc f (i + k + (N + 1)) ≤ r ^ (i + k + (N + 1)) := f_le _

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 84 at dc94c2f71b52 ↗

    2. term_le.s2 calc routine: ring

      Closes the goal.

      Lean, line 85
            _ = r ^ (k + (N + 1)) * r ^ i := by ring

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 85 at dc94c2f71b52 ↗

    3. term_le.s3 calc r ^ (k + (N + (1 : ℕ))) * r ^ i ≤ r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left, pow_le_pow_left₀, pow_nonneg.

      Lean, lines 86–87
            _ ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ r0.le r2 i) (pow_nonneg r0.le _)

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 86–87 at dc94c2f71b52 ↗

  26. Rle have R ≤ r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)

    Leaves False, with Rle : R ≤ r ^ (k + (N + (1 : ℕ))) * (2 : ℝ).

    Lean, lines 88–92
      have Rle : R ≤ r ^ (k + (N + 1)) * 2 := by
    rw [hR]
    calc ∑' i, f (i + k + (N + 1)) ≤ ∑' i : ℕ, r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
          Summable.tsum_le_tsum term_le hg' geo
      _ = r ^ (k + (N + 1)) * 2 := by rw [tsum_mul_left, tsum_geometric_two]

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 88–92 at dc94c2f71b52 ↗

    1. Rle.s1 calc ∑' (i : ℕ), f (i + k + (N + (1 : ℕ))) ≤ ∑' (i : ℕ), r ^ (k + (N + (1 : ℕ))) * (1 / 2 : ℝ) ^ i

      Closes the goal.

      Uses library Summable.tsum_le_tsum.

      Lean, lines 90–91
          calc ∑' i, f (i + k + (N + 1)) ≤ ∑' i : ℕ, r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
          Summable.tsum_le_tsum term_le hg' geo

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 90–91 at dc94c2f71b52 ↗

    2. Rle.s2 calc

      Closes the goal.

      Uses library tsum_mul_left, tsum_geometric_two.

      Lean, line 92
            _ = r ^ (k + (N + 1)) * 2 := by rw [tsum_mul_left, tsum_geometric_two]

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 92 at dc94c2f71b52 ↗

  27. bN have (↑b : ℝ) ^ N * r ^ N = (1 : ℝ)

    Leaves False, with bN : (↑b : ℝ) ^ N * r ^ N = (1 : ℝ).

    Uses library mul_pow, mul_comm, one_pow.

    Lean, line 93
      have bN : (b : ℝ) ^ N * r ^ N = 1 := by rw [← mul_pow, mul_comm, rb, one_pow]

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 93 at dc94c2f71b52 ↗

  28. key have (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) ≤ r ^ k

    Leaves False, with key : (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) ≤ r ^ k.

    Uses library mul_one.

    Lean, lines 94–100
      have key : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2) ≤ r ^ k := by
    have e : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2)
        = r ^ k * ((b : ℝ) ^ N * r ^ N) * (2 * r) := by ring
    rw [e, bN, mul_one]
    have h2r : 2 * r ≤ 1 := by linarith
    calc r ^ k * (2 * r) ≤ r ^ k * 1 := mul_le_mul_of_nonneg_left h2r (pow_nonneg r0.le k)
      _ = r ^ k := mul_one _

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 94–100 at dc94c2f71b52 ↗

    1. key.e have (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = r ^ k * ((↑b : ℝ) ^ N * r ^ N) * ((2 : ℝ) * r) routine: ring

      Leaves (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) ≤ r ^ k, with e : (↑b : ℝ) ^ N * (r ^ (k + (N + (1 : ℕ))) * (2 : ℝ)) = r ^ k * ((↑b : ℝ) ^ N * r ^ N) * ((2 : ℝ) * r).

      Lean, lines 95–96
          have e : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2)
        = r ^ k * ((b : ℝ) ^ N * r ^ N) * (2 * r) := by ring

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 95–96 at dc94c2f71b52 ↗

    2. key.h2r have (2 : ℝ) * r ≤ (1 : ℝ) routine: linarith

      Leaves r ^ k * ((2 : ℝ) * r) ≤ r ^ k, with h2r : (2 : ℝ) * r ≤ (1 : ℝ).

      Lean, line 98
          have h2r : 2 * r ≤ 1 := by linarith

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 98 at dc94c2f71b52 ↗

    3. key.s3 calc r ^ k * ((2 : ℝ) * r) ≤ r ^ k * (1 : ℝ)

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left, pow_nonneg.

      Lean, line 99
          calc r ^ k * (2 * r) ≤ r ^ k * 1 := mul_le_mul_of_nonneg_left h2r (pow_nonneg r0.le k)

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 99 at dc94c2f71b52 ↗

    4. key.s4 calc r ^ k * (1 : ℝ) = r ^ k

      Closes the goal.

      Uses library mul_one.

      Lean, line 100
            _ = r ^ k := mul_one _

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 100 at dc94c2f71b52 ↗

  29. s29 obtain ∃ (Z : ℕ), Z = ∑ i ∈ Finset.range (N + (1 : ℕ)), if Nat.Prime i then b ^ (N - i) else (0 : ℕ)

    Leaves False, with Z : ℕ, hZ : Z = ∑ i ∈ Finset.range (N + (1 : ℕ)), if Nat.Prime i then b ^ (N - i) else (0 : ℕ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 101–102
      obtain ⟨Z, hZ⟩ : ∃ Z : ℕ,
      Z = ∑ i ∈ Finset.range (N + 1), if i.Prime then b ^ (N - i) else 0 := ⟨_, rfl⟩

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 101–102 at dc94c2f71b52 ↗

  30. hZ' have (↑b : ℝ) ^ N * ∑ i ∈ Finset.range (N + (1 : ℕ)), f i = (↑Z : ℝ)

    Leaves False, with hZ' : (↑b : ℝ) ^ N * ∑ i ∈ Finset.range (N + (1 : ℕ)), f i = (↑Z : ℝ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mul_sum, Finset.sum_congr, rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 103–113
      have hZ' : (b : ℝ) ^ 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 : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow, mul_comm (b : ℝ) r, rb, one_pow, mul_one]
    · simp

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 103–113 at dc94c2f71b52 ↗

    1. hZ'.hi' have i ≤ N

      Leaves (↑b : ℝ) ^ N * f i = if Nat.Prime i then (↑b : ℝ) ^ (N - i) else (0 : ℝ), with hi' : i ≤ N.

      Uses library Nat.lt_succ_iff, Finset.mem_range.

      Lean, line 107
          have hi' : i ≤ N := Nat.lt_succ_iff.mp (Finset.mem_range.mp hi)

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 107 at dc94c2f71b52 ↗

    2. hZ'.s2 case

      Leaves (↑b : ℝ) ^ N * r ^ i = (↑b : ℝ) ^ (N - i).

      Uses library mul_assoc, mul_pow, mul_comm, one_pow, mul_one.

      Lean, lines 110–112
          · have e : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow, mul_comm (b : ℝ) r, rb, one_pow, mul_one]

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 110–112 at dc94c2f71b52 ↗

      1. hZ'.s2.e have (↑b : ℝ) ^ N = (↑b : ℝ) ^ (N - i) * (↑b : ℝ) ^ i

        Leaves (↑b : ℝ) ^ N * r ^ i = (↑b : ℝ) ^ (N - i), with e : (↑b : ℝ) ^ N = (↑b : ℝ) ^ (N - i) * (↑b : ℝ) ^ i.

        Uses library pow_add, Nat.sub_add_cancel.

        Lean, lines 110–111
            · have e : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 110–111 at dc94c2f71b52 ↗

    3. hZ'.s3 case routine: simp

      Leaves (↑b : ℝ) ^ N * (0 : ℝ) = (0 : ℝ).

      Lean, line 113
          · simp

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 113 at dc94c2f71b52 ↗

  31. hqk have (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ)

    Leaves False, with hqk : (↑q : ℝ) * (↑k : ℝ) = (↑q.num : ℝ).

    Uses library Rat.mul_den_eq_num.

    Lean, line 114
      have hqk : (q : ℝ) * k = q.num := by rw [hk]; exact_mod_cast Rat.mul_den_eq_num q

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 114 at dc94c2f71b52 ↗

  32. 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 range n is the set of natural numbers less than n. .

    Lean, lines 115–116
      have hx : (q : ℝ) = ∑ i ∈ Finset.range (N + 1), f i + R := by
    rw [hq, ← split1, split2']

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 115–116 at dc94c2f71b52 ↗

  33. hm have (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((↑b : ℝ) ^ N * R)

    Leaves False, with hm : (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) = (↑k : ℝ) * ((↑b : ℝ) ^ N * R).

    Lean, lines 117–119
      have hm : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) = (k : ℝ) * ((b : ℝ) ^ N * R) := by
    push_cast
    rw [← hqk, hx, ← hZ']; ring

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 117–119 at dc94c2f71b52 ↗

  34. kR have (0 : ℝ) < (↑k : ℝ)

    Leaves False, with kR : (0 : ℝ) < (↑k : ℝ).

    Lean, line 120
      have kR : (0 : ℝ) < k := by exact_mod_cast kpos

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 120 at dc94c2f71b52 ↗

  35. mpos have (0 : ℝ) < (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ)

    Leaves False, with mpos : (0 : ℝ) < (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ).

    Uses library mul_pos Alias of Left.mul_pos. , pow_pos.

    Lean, lines 121–122
      have mpos : (0 : ℝ) < (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) := by
    rw [hm]; exact mul_pos kR (mul_pos (pow_pos bpos N) Rpos)

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 121–122 at dc94c2f71b52 ↗

  36. mlt have (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ)

    Leaves False, with mlt : (↑((↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)) : ℝ) < (1 : ℝ).

    Lean, lines 123–134
      have mlt : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) < 1 := by
    rw [hm]
    have h2 : (b : ℝ) ^ N * R ≤ r ^ k :=
      le_trans (mul_le_mul_of_nonneg_left Rle (pow_nonneg bpos.le N)) key
    have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hkb : (k : ℝ) * r ^ k < 1 := by
      have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]
      rw [e, div_lt_one (pow_pos bpos k)]
      calc (k : ℝ) < 2 ^ k := hk2
        _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k
    calc (k : ℝ) * ((b : ℝ) ^ N * R) ≤ k * r ^ k := mul_le_mul_of_nonneg_left h2 kR.le
      _ < 1 := hkb

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 123–134 at dc94c2f71b52 ↗

    1. mlt.h2 have (↑b : ℝ) ^ N * R ≤ r ^ k

      Leaves (↑k : ℝ) * ((↑b : ℝ) ^ N * R) < (1 : ℝ), with h2 : (↑b : ℝ) ^ N * R ≤ r ^ k.

      Uses library le_trans The relation ≤ on a preorder is transitive. , mul_le_mul_of_nonneg_left, pow_nonneg.

      Lean, lines 125–126
          have h2 : (b : ℝ) ^ N * R ≤ r ^ k :=
      le_trans (mul_le_mul_of_nonneg_left Rle (pow_nonneg bpos.le N)) key

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 125–126 at dc94c2f71b52 ↗

    2. mlt.hk2 have (↑k : ℝ) < (2 : ℝ) ^ k

      Leaves (↑k : ℝ) * ((↑b : ℝ) ^ N * R) < (1 : ℝ), with hk2 : (↑k : ℝ) < (2 : ℝ) ^ k.

      Uses library Nat.lt_two_pow_self.

      Lean, line 127
          have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 127 at dc94c2f71b52 ↗

    3. mlt.hkb have (↑k : ℝ) * r ^ k < (1 : ℝ)

      Leaves (↑k : ℝ) * ((↑b : ℝ) ^ N * R) < (1 : ℝ), with hkb : (↑k : ℝ) * r ^ k < (1 : ℝ).

      Uses library div_lt_one, pow_pos.

      Lean, lines 128–132
          have hkb : (k : ℝ) * r ^ k < 1 := by
      have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]
      rw [e, div_lt_one (pow_pos bpos k)]
      calc (k : ℝ) < 2 ^ k := hk2
        _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, lines 128–132 at dc94c2f71b52 ↗

      1. mlt.hkb.e have (↑k : ℝ) * r ^ k = (↑k : ℝ) / (↑b : ℝ) ^ k

        Leaves (↑k : ℝ) * r ^ k < (1 : ℝ), with e : (↑k : ℝ) * r ^ k = (↑k : ℝ) / (↑b : ℝ) ^ k.

        Uses library div_pow, one_pow, mul_one_div.

        Lean, line 129
              have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 129 at dc94c2f71b52 ↗

      2. mlt.hkb.s2 calc (↑k : ℝ) < (2 : ℝ) ^ k

        Closes the goal.

        Lean, line 131
              calc (k : ℝ) < 2 ^ k := hk2

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 131 at dc94c2f71b52 ↗

      3. mlt.hkb.s3 calc (2 : ℝ) ^ k ≤ (↑b : ℝ) ^ k

        Closes the goal.

        Uses library pow_le_pow_left₀.

        Lean, line 132
                _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k

        targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 132 at dc94c2f71b52 ↗

    4. mlt.s4 calc (↑k : ℝ) * ((↑b : ℝ) ^ N * R) ≤ (↑k : ℝ) * r ^ k

      Closes the goal.

      Uses library mul_le_mul_of_nonneg_left.

      Lean, line 133
          calc (k : ℝ) * ((b : ℝ) ^ N * R) ≤ k * r ^ k := mul_le_mul_of_nonneg_left h2 kR.le

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 133 at dc94c2f71b52 ↗

    5. mlt.s5 calc (↑k : ℝ) * r ^ k < (1 : ℝ)

      Closes the goal.

      Lean, line 134
            _ < 1 := hkb

      targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 134 at dc94c2f71b52 ↗

  37. i1 have (0 : ℤ) < (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ)

    Leaves False, with i1 : (0 : ℤ) < (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ).

    Lean, line 135
      have i1 : (0 : ℤ) < (b : ℤ) ^ N * q.num - k * Z := by exact_mod_cast mpos

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 135 at dc94c2f71b52 ↗

  38. i2 have (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ)

    Leaves False, with i2 : (↑b : ℤ) ^ N * q.num - (↑k : ℤ) * (↑Z : ℤ) < (1 : ℤ).

    Lean, line 136
      have i2 : (b : ℤ) ^ N * q.num - k * Z < 1 := by exact_mod_cast mlt

    targets/erdos-69/nodes/variant-f592e3ab/Proof.lean, line 136 at dc94c2f71b52 ↗

The proof in Lean (Proof.lean)

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

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-f592e3ab/Proof.lean, sha256 23537c88ca6c.
import Mathlib
import Nodes.«variant-f592e3ab».Context

/-! A related variant of Erdős problem 69 (D-30, relation `related`): for every base `b ≥ 2`,
the number `∑_{p prime} b^{-p}`, whose base-`b` digits are 1 exactly at the prime places, is
irrational.

Why it sits beside erdos-69: it is the root's series `∑ ω(n)/2^n` with `ω(n)` replaced by the
prime indicator, and with the base 2 generalised to any `b ≥ 2`. The base-2 case is already
proved on this target as `variant-09e95e7a`; this statement is the strict generalisation, by
the same method: the `k` integers `(k+1)! + 2, …, (k+1)! + k + 1` are composite, so if the sum
were `a/k` the digits after place `N = (k+1)! + 1` would be zero for `k` places and not zero
for ever after, making `k · b^N · (tail)` an integer strictly between 0 and 1. It is not
progress on the root, whose hard part (the digits of `∑ ω(n)/2^n` are not eventually periodic)
this method does not reach. -/

theorem Opn.erdos_69_primes_any_base :
    ∀ b : ℕ, 2 ≤ b → Irrational (∑' p : Nat.Primes, (1 : ℝ) / (b : ℝ) ^ (p : ℕ)) := by
  intro b hb
  have hb0 : (2 : ℝ) ≤ (b : ℝ) := by exact_mod_cast hb
  have bpos : (0 : ℝ) < b := by linarith
  obtain ⟨r, hr⟩ : ∃ r : ℝ, r = 1 / (b : ℝ) := ⟨_, rfl⟩
  have r0 : 0 < r := by rw [hr]; exact one_div_pos.mpr bpos
  have r2 : r ≤ 1 / 2 := by rw [hr]; exact one_div_le_one_div_of_le (by norm_num) hb0
  have rb : r * (b : ℝ) = 1 := by rw [hr, one_div, inv_mul_cancel₀ bpos.ne']
  obtain ⟨f, hf⟩ : ∃ f : ℕ → ℝ, f = fun n => if n.Prime then r ^ n else 0 := ⟨_, rfl⟩
  have hconv : ∑' p : Nat.Primes, (1 : ℝ) / (b : ℝ) ^ (p : ℕ) = ∑' n : ℕ, f n := by
    have h := tsum_subtype {p : ℕ | p.Prime} (fun n : ℕ => (1 : ℝ) / (b : ℝ) ^ n)
    refine h.trans ?_
    congr 1; funext n
    simp only [Set.indicator_apply, Set.mem_ofPred_eq, hf, hr, one_div_pow]
  rw [hconv]
  have f_nonneg : ∀ n, 0 ≤ f n := fun n => by
    simp only [hf]; split_ifs
    · exact pow_nonneg r0.le n
    · exact le_rfl
  have f_le : ∀ n, f n ≤ r ^ n := fun n => by
    simp only [hf]; split_ifs
    · exact le_rfl
    · exact pow_nonneg r0.le n
  have hs : Summable f :=
    Summable.of_nonneg_of_le f_nonneg f_le
      (summable_geometric_of_lt_one r0.le (by linarith))
  rintro ⟨q, hq⟩
  obtain ⟨k, hk⟩ : ∃ k, k = q.den := ⟨_, rfl⟩
  have kpos : 0 < k := by rw [hk]; exact q.den_pos
  obtain ⟨N, hN⟩ : ∃ N, N = (k + 1).factorial + 1 := ⟨_, rfl⟩
  have comp : ∀ j, j < k → f (j + (N + 1)) = 0 := by
    intro j hj
    simp only [hf]
    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
    exact comp j (Finset.mem_range.mp hj)
  obtain ⟨R, hR⟩ : ∃ R, R = ∑' i, f (i + k + (N + 1)) := ⟨_, rfl⟩
  have split2' : ∑' i, f (i + (N + 1)) = R := by
    rw [← split2, zero_part, zero_add, hR]
  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
    rw [hR]
    refine hg'.tsum_pos (fun i => f_nonneg _) (p - (k + (N + 1))) ?_
    rw [hpi]; simp only [hf, if_pos hp2]; exact pow_pos r0 p
  have geo : Summable (fun i : ℕ => r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i) :=
    summable_geometric_two.mul_left _
  have term_le : ∀ i, f (i + k + (N + 1)) ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i := by
    intro i
    calc f (i + k + (N + 1)) ≤ r ^ (i + k + (N + 1)) := f_le _
      _ = r ^ (k + (N + 1)) * r ^ i := by ring
      _ ≤ r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
        mul_le_mul_of_nonneg_left (pow_le_pow_left₀ r0.le r2 i) (pow_nonneg r0.le _)
  have Rle : R ≤ r ^ (k + (N + 1)) * 2 := by
    rw [hR]
    calc ∑' i, f (i + k + (N + 1)) ≤ ∑' i : ℕ, r ^ (k + (N + 1)) * (1 / 2 : ℝ) ^ i :=
          Summable.tsum_le_tsum term_le hg' geo
      _ = r ^ (k + (N + 1)) * 2 := by rw [tsum_mul_left, tsum_geometric_two]
  have bN : (b : ℝ) ^ N * r ^ N = 1 := by rw [← mul_pow, mul_comm, rb, one_pow]
  have key : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2) ≤ r ^ k := by
    have e : (b : ℝ) ^ N * (r ^ (k + (N + 1)) * 2)
        = r ^ k * ((b : ℝ) ^ N * r ^ N) * (2 * r) := by ring
    rw [e, bN, mul_one]
    have h2r : 2 * r ≤ 1 := by linarith
    calc r ^ k * (2 * r) ≤ r ^ k * 1 := mul_le_mul_of_nonneg_left h2r (pow_nonneg r0.le k)
      _ = r ^ k := mul_one _
  obtain ⟨Z, hZ⟩ : ∃ Z : ℕ,
      Z = ∑ i ∈ Finset.range (N + 1), if i.Prime then b ^ (N - i) else 0 := ⟨_, rfl⟩
  have hZ' : (b : ℝ) ^ 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 : (b : ℝ) ^ N = (b : ℝ) ^ (N - i) * (b : ℝ) ^ i := by
        rw [← pow_add, Nat.sub_add_cancel hi']
      rw [e, mul_assoc, ← mul_pow, mul_comm (b : ℝ) r, rb, one_pow, mul_one]
    · simp
  have hqk : (q : ℝ) * k = q.num := by rw [hk]; exact_mod_cast Rat.mul_den_eq_num q
  have hx : (q : ℝ) = ∑ i ∈ Finset.range (N + 1), f i + R := by
    rw [hq, ← split1, split2']
  have hm : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) = (k : ℝ) * ((b : ℝ) ^ N * R) := by
    push_cast
    rw [← hqk, hx, ← hZ']; ring
  have kR : (0 : ℝ) < k := by exact_mod_cast kpos
  have mpos : (0 : ℝ) < (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) := by
    rw [hm]; exact mul_pos kR (mul_pos (pow_pos bpos N) Rpos)
  have mlt : (((b : ℤ) ^ N * q.num - k * Z : ℤ) : ℝ) < 1 := by
    rw [hm]
    have h2 : (b : ℝ) ^ N * R ≤ r ^ k :=
      le_trans (mul_le_mul_of_nonneg_left Rle (pow_nonneg bpos.le N)) key
    have hk2 : (k : ℝ) < 2 ^ k := by exact_mod_cast Nat.lt_two_pow_self
    have hkb : (k : ℝ) * r ^ k < 1 := by
      have e : (k : ℝ) * r ^ k = k / (b : ℝ) ^ k := by rw [hr, div_pow, one_pow, mul_one_div]
      rw [e, div_lt_one (pow_pos bpos k)]
      calc (k : ℝ) < 2 ^ k := hk2
        _ ≤ (b : ℝ) ^ k := pow_le_pow_left₀ (by norm_num) hb0 k
    calc (k : ℝ) * ((b : ℝ) ^ N * R) ≤ k * r ^ k := mul_le_mul_of_nonneg_left h2 kR.le
      _ < 1 := hkb
  have i1 : (0 : ℤ) < (b : ℤ) ^ N * q.num - k * Z := by exact_mod_cast mpos
  have i2 : (b : ℤ) ^ N * q.num - k * Z < 1 := by exact_mod_cast mlt
  omega

What is known

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).

Write the explainer →

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

/-! A related variant of Erdős problem 69 (D-30, relation `related`): for every base `b ≥ 2`,
the number `∑_{p prime} b^{-p}`, whose base-`b` digits are 1 exactly at the prime places, is
irrational.

Why it sits beside erdos-69: it is the root's series `∑ ω(n)/2^n` with `ω(n)` replaced by the
prime indicator, and with the base 2 generalised to any `b ≥ 2`. The base-2 case is already
proved on this target as `variant-09e95e7a`; this statement is the strict generalisation, by
the same method: the `k` integers `(k+1)! + 2, …, (k+1)! + k + 1` are composite, so if the sum
were `a/k` the digits after place `N = (k+1)! + 1` would be zero for `k` places and not zero
for ever after, making `k · b^N · (tail)` an integer strictly between 0 and 1. It is not
progress on the root, whose hard part (the digits of `∑ ω(n)/2^n` are not eventually periodic)
this method does not reach. -/

theorem Opn.erdos_69_primes_any_base :
    ∀ b : ℕ, 2 ≤ b → Irrational (∑' p : Nat.Primes, (1 : ℝ) / (b : ℝ) ^ (p : ℕ)) := by
  sorry

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

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 \forall b\in\mathbb{N},\ b\ge 2:\quad \sum_{p\ \text{prime}}\frac{1}{b^{p}} \notin\mathbb{Q}$

For every natural base b ≥ 2, the sum over the primes p of 1/b^p, in ℝ, is irrational. The series is a tsum over ℝ (0 when not summable), and Irrational x means x is not the cast of a rational.

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000300.json, merge commit dc94c2f71b52.

Verdict pass, from attestations/000300.json.

Submitter
t0929-3
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000300.json, merge commit dc94c2f71b52.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-69/nodes/variant-f592e3ab/Witness.lean, sha256 1b585e251109.
theorem witness : ∃ b : ℕ, 2 ≤ b := ⟨2, le_rfl⟩

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 (2)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at 1 / ↑b ^ ↑p

The divisor is b^p with b ≥ 2 by hypothesis, so it is never 0 and no term takes Lean's junk value.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a off-by-one-range finding at 2 ≤ b

Inclusive on purpose: bases b ≥ 2 are exactly those where the series is a base-b expansion (b = 1 diverges to the junk value 0 of tsum, b = 0 is junk).

How to read this page

How to read a statement’s page →