FormalConjectures.OEIS.«86766»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Smallest $r$ such that (concatenation of $n$, $r$ times) $\cdot 10 + 1$ is prime

$a(n)$ is the smallest $r$ where (concatenation of $n$, $r$ times with itself) $\cdot 10 + 1$ is a prime, or $0$ if no such number exists. The number resulting from concatenating $n$, $r$ times, is $n \cdot \sum_{i=0}^{r-1} (10^d)^i$, where $d$ is the number of digits of $n$.

References:

A086766

namespace OeisA86766

Sequence $a(n)$ is the smallest $r > 0$ such that the concatenation of $n$, $r$ times with itself, multiplied by $10$ plus $1$, is prime, or $0$ if no such prime exists.

noncomputable def a (n : ℕ) : ℕ :=
  if n = 0 then 0
  else
    let ℓ : ℕ := (Nat.digits 10 n).length
    let M : ℕ := 10 ^ ℓ
    let repCatVal (r : ℕ) : ℕ := n * ∑ i ∈ Finset.range r, M ^ i
    let primeCandidate (r : ℕ) : ℕ := repCatVal r * 10 + 1
    sInf {r : ℕ | 0 < r ∧ (primeCandidate r).Prime}

Value of the sequence a at 0.

@[category test, AMS 11]
theorem a_0 : a 0 = 0 := by⊢ a 0 = 0 rflAll goals completed! 🐙

Value of the sequence a at 1.


@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1
  have h_least : IsLeast {r : ℕ | 0 < r ∧ ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  1).length) ^ i) * 10 + 1).Prime} 1 := by
    constructorleft⊢ 1 ∈ {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}right⊢ 1 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
    ·left⊢ 1 ∈ {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1 simp only [Set.mem_ofPred_eq]left⊢ 0 < 1 ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
      refine ⟨by⊢ 0 < 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1 omegaAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1, ?_⟩
      have : (Nat.digits 10 1).length = 1 := by⊢ a 1 = 1leftthis:(Nat.digits 10 1).length = 1⊢ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1 decide +nativeleftthis:(Nat.digits 10 1).length = 1⊢ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1leftthis:(Nat.digits 10 1).length = 1⊢ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
      rw [thisleftthis:(Nat.digits 10 1).length = 1⊢ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)leftthis:(Nat.digits 10 1).length = 1⊢ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1]leftthis:(Nat.digits 10 1).length = 1⊢ Nat.Prime ((1 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
      norm_numAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
    ·right⊢ 1 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1 intro r hrrightr:ℕhr:r ∈ {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ 1 ≤ rh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
      simp only [Set.mem_ofPred_eq] at hrrightr:ℕhr:0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)⊢ 1 ≤ rh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
      exact hr.1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ a 1 = 1
  have ha1 : a 1 = sInf {r : ℕ | 0 < r ∧ ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  1).length) ^ i) * 10 + 1).Prime} := by
    unfold ah_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1⊢ (if 1 = 0 then 0
  else
    have ℓ := (Nat.digits 10 1).length;
    have M := 10 ^ ℓ;
    have repCatVal := fun r ↦ 1 * ∑ i ∈ Finset.range r, M ^ i;
    have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
    sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ a 1 = 1
    splitisTrueh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1h✝:1 = 0⊢ 0 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}isFalseh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1h✝:¬1 = 0⊢ (have ℓ := (Nat.digits 10 1).length;
  have M := 10 ^ ℓ;
  have repCatVal := fun r ↦ 1 * ∑ i ∈ Finset.range r, M ^ i;
  have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
  sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ a 1 = 1 <;> [omegaAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ a 1 = 1; rflAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ a 1 = 1]h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ a 1 = 1
  rw [ha1,h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} = 1All goals completed! 🐙 h_least.csInf_eqh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)} 1ha1:a 1 = sInf {r | 0 < r ∧ Nat.Prime ((1 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 1).length) ^ i) * 10 + 1)}⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

Value of the sequence a at 2.


@[category test, AMS 11]
theorem a_2 : a 2 = 3 := by⊢ a 2 = 3
  have h_digits : (Nat.digits 10 2).length = 1 := by decide +nativeh_digits:(Nat.digits 10 2).length = 1⊢ a 2 = 3h_digits:(Nat.digits 10 2).length = 1⊢ a 2 = 3
  have h_least : IsLeast {r : ℕ | 0 < r ∧ ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  2).length) ^ i) * 10 + 1).Prime} 3 := by
    constructorlefth_digits:(Nat.digits 10 2).length = 1⊢ 3 ∈ {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}righth_digits:(Nat.digits 10 2).length = 1⊢ 3 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
    ·lefth_digits:(Nat.digits 10 2).length = 1⊢ 3 ∈ {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3 simp only [Set.mem_ofPred_eq]lefth_digits:(Nat.digits 10 2).length = 1⊢ 0 < 3 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 3, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      refine ⟨byh_digits:(Nat.digits 10 2).length = 1⊢ 0 < 3h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3 omegaAll goals completed! 🐙h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3, ?_⟩
      rw [h_digitslefth_digits:(Nat.digits 10 2).length = 1⊢ Nat.Prime ((2 * ∑ i ∈ Finset.range 3, (10 ^ 1) ^ i) * 10 + 1)lefth_digits:(Nat.digits 10 2).length = 1⊢ Nat.Prime ((2 * ∑ i ∈ Finset.range 3, (10 ^ 1) ^ i) * 10 + 1)h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3]lefth_digits:(Nat.digits 10 2).length = 1⊢ Nat.Prime ((2 * ∑ i ∈ Finset.range 3, (10 ^ 1) ^ i) * 10 + 1)h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      norm_numAll goals completed! 🐙h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
    ·righth_digits:(Nat.digits 10 2).length = 1⊢ 3 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3 intro r hrrighth_digits:(Nat.digits 10 2).length = 1r:ℕhr:r ∈ {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ 3 ≤ rh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      simp only [Set.mem_ofPred_eq] at hrrighth_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)⊢ 3 ≤ rh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      by_contra! hrighth_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:r < 3⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      have hr_pos := hr.1righth_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:r < 3hr_pos:0 < r⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      interval_cases rright.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1⊢ Falseright.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      ·right.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3 have hr2 := hr.2right.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
        rw [h_digitsright.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)⊢ Falseright.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3] at hr2right.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
        revert hr2right.«1»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 1 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:1 < 3hr_pos:0 < 1⊢ Nat.Prime ((2 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1) → Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
        norm_numAll goals completed! 🐙h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
      ·right.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3 have hr2 := hr.2right.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
        rw [h_digitsright.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ 1) ^ i) * 10 + 1)⊢ Falseright.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ 1) ^ i) * 10 + 1)⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3] at hr2right.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2hr2:Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ 1) ^ i) * 10 + 1)⊢ Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
        revert hr2right.«2»h_digits:(Nat.digits 10 2).length = 1r:ℕhr:0 < 2 ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)h:2 < 3hr_pos:0 < 2⊢ Nat.Prime ((2 * ∑ i ∈ Finset.range 2, (10 ^ 1) ^ i) * 10 + 1) → Falseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
        norm_numh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ a 2 = 3
  have ha2 : a 2 = sInf {r : ℕ | 0 < r ∧ ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  2).length) ^ i) * 10 + 1).Prime} := by
    unfold ah_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3⊢ (if 2 = 0 then 0
  else
    have ℓ := (Nat.digits 10 2).length;
    have M := 10 ^ ℓ;
    have repCatVal := fun r ↦ 2 * ∑ i ∈ Finset.range r, M ^ i;
    have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
    sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ a 2 = 3
    splitisTrueh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3h✝:2 = 0⊢ 0 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}isFalseh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3h✝:¬2 = 0⊢ (have ℓ := (Nat.digits 10 2).length;
  have M := 10 ^ ℓ;
  have repCatVal := fun r ↦ 2 * ∑ i ∈ Finset.range r, M ^ i;
  have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
  sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ a 2 = 3 <;> [omegaAll goals completed! 🐙h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ a 2 = 3; rflAll goals completed! 🐙h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ a 2 = 3]h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ a 2 = 3
  rw [ha2,h_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} = 3All goals completed! 🐙 h_least.csInf_eqh_digits:(Nat.digits 10 2).length = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)} 3ha2:a 2 = sInf {r | 0 < r ∧ Nat.Prime ((2 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 2).length) ^ i) * 10 + 1)}⊢ 3 = 3All goals completed! 🐙]All goals completed! 🐙

Value of the sequence a at 3.


@[category test, AMS 11]
theorem a_3 : a 3 = 1 := by⊢ a 3 = 1
  have h_least : IsLeast {r : ℕ | 0 < r ∧ ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  3).length) ^ i) * 10 + 1).Prime} 1 := by
    constructorleft⊢ 1 ∈ {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}right⊢ 1 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
    ·left⊢ 1 ∈ {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1 simp only [Set.mem_ofPred_eq]left⊢ 0 < 1 ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
      refine ⟨by⊢ 0 < 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1 omegaAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1, ?_⟩
      have : (Nat.digits 10 3).length = 1 := by⊢ a 3 = 1leftthis:(Nat.digits 10 3).length = 1⊢ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1 decide +nativeleftthis:(Nat.digits 10 3).length = 1⊢ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1leftthis:(Nat.digits 10 3).length = 1⊢ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
      rw [thisleftthis:(Nat.digits 10 3).length = 1⊢ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)leftthis:(Nat.digits 10 3).length = 1⊢ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1]leftthis:(Nat.digits 10 3).length = 1⊢ Nat.Prime ((3 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
      norm_numAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
    ·right⊢ 1 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1 intro r hrrightr:ℕhr:r ∈ {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ 1 ≤ rh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
      simp only [Set.mem_ofPred_eq] at hrrightr:ℕhr:0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)⊢ 1 ≤ rh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
      exact hr.1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ a 3 = 1
  have ha3 : a 3 = sInf {r : ℕ | 0 < r ∧ ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  3).length) ^ i) * 10 + 1).Prime} := by
    unfold ah_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1⊢ (if 3 = 0 then 0
  else
    have ℓ := (Nat.digits 10 3).length;
    have M := 10 ^ ℓ;
    have repCatVal := fun r ↦ 3 * ∑ i ∈ Finset.range r, M ^ i;
    have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
    sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ a 3 = 1
    splitisTrueh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1h✝:3 = 0⊢ 0 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}isFalseh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1h✝:¬3 = 0⊢ (have ℓ := (Nat.digits 10 3).length;
  have M := 10 ^ ℓ;
  have repCatVal := fun r ↦ 3 * ∑ i ∈ Finset.range r, M ^ i;
  have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
  sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ a 3 = 1 <;> [omegaAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ a 3 = 1; rflAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ a 3 = 1]h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ a 3 = 1
  rw [ha3,h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} = 1All goals completed! 🐙 h_least.csInf_eqh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)} 1ha3:a 3 = sInf {r | 0 < r ∧ Nat.Prime ((3 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 3).length) ^ i) * 10 + 1)}⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

Value of the sequence a at 4.


@[category test, AMS 11]
theorem a_4 : a 4 = 1 := by⊢ a 4 = 1
  have h_least : IsLeast {r : ℕ | 0 < r ∧ ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  4).length) ^ i) * 10 + 1).Prime} 1 := by
    constructorleft⊢ 1 ∈ {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}right⊢ 1 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
    ·left⊢ 1 ∈ {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1 simp only [Set.mem_ofPred_eq]left⊢ 0 < 1 ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
      refine ⟨by⊢ 0 < 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1 omegaAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1, ?_⟩
      have : (Nat.digits 10 4).length = 1 := by⊢ a 4 = 1leftthis:(Nat.digits 10 4).length = 1⊢ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1 decide +nativeleftthis:(Nat.digits 10 4).length = 1⊢ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1leftthis:(Nat.digits 10 4).length = 1⊢ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
      rw [thisleftthis:(Nat.digits 10 4).length = 1⊢ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)leftthis:(Nat.digits 10 4).length = 1⊢ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1]leftthis:(Nat.digits 10 4).length = 1⊢ Nat.Prime ((4 * ∑ i ∈ Finset.range 1, (10 ^ 1) ^ i) * 10 + 1)h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
      norm_numAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
    ·right⊢ 1 ∈ lowerBounds {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1 intro r hrrightr:ℕhr:r ∈ {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ 1 ≤ rh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
      simp only [Set.mem_ofPred_eq] at hrrightr:ℕhr:0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)⊢ 1 ≤ rh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
      exact hr.1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ a 4 = 1
  have ha4 : a 4 = sInf {r : ℕ | 0 < r ∧ ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10
  4).length) ^ i) * 10 + 1).Prime} := by
    unfold ah_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1⊢ (if 4 = 0 then 0
  else
    have ℓ := (Nat.digits 10 4).length;
    have M := 10 ^ ℓ;
    have repCatVal := fun r ↦ 4 * ∑ i ∈ Finset.range r, M ^ i;
    have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
    sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ a 4 = 1
    splitisTrueh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1h✝:4 = 0⊢ 0 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}isFalseh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1h✝:¬4 = 0⊢ (have ℓ := (Nat.digits 10 4).length;
  have M := 10 ^ ℓ;
  have repCatVal := fun r ↦ 4 * ∑ i ∈ Finset.range r, M ^ i;
  have primeCandidate := fun r ↦ repCatVal r * 10 + 1;
  sInf {r | 0 < r ∧ Nat.Prime (primeCandidate r)}) =
  sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ a 4 = 1 <;> [omegaAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ a 4 = 1; rflAll goals completed! 🐙h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ a 4 = 1]h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ a 4 = 1
  rw [ha4,h_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} = 1All goals completed! 🐙 h_least.csInf_eqh_least:IsLeast {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)} 1ha4:a 4 = sInf {r | 0 < r ∧ Nat.Prime ((4 * ∑ i ∈ Finset.range r, (10 ^ (Nat.digits 10 4).length) ^ i) * 10 + 1)}⊢ 1 = 1All goals completed! 🐙]All goals completed! 🐙

open scoped Classical in

What is the smallest integer $m > 1$ such that $a(10^m)$ is nonzero?

Farideh Firoozbakht, Jan 07 2015

@[category research open, AMS 11]
theorem conjecture1 :
    answer(sorry) =
      if h : ∃ m, 1 < m ∧ a (10 ^ m) ≠ 0 then
        some (sInf {m | 1 < m ∧ a (10 ^ m) ≠ 0})
      else
        none := by⊢ sorry = if h : ∃ m, 1 < m ∧ a (10 ^ m) ≠ 0 then some (sInf {m | 1 < m ∧ a (10 ^ m) ≠ 0}) else none
  sorryAll goals completed! 🐙

Conjecture: If $n$ is not of the form $10^m$ then $a(n)$ is nonzero.

Farideh Firoozbakht, Jan 07 2015

@[category research open, AMS 11]
theorem conjecture2 (n : ℕ) (hn : 0 < n) (h : ∀ m : ℕ, n ≠ 10 ^ m) : a n ≠ 0 := byn:ℕhn:0 < nh:∀ (m : ℕ), n ≠ 10 ^ m⊢ a n ≠ 0
  sorryAll goals completed! 🐙

open scoped Classical in

What is the smallest odd prime $p$ such that $(10^{p^2}-1)/(10^p-1)$ is a prime number (and $a(10^{p-1})$ could be nonzero)?

Farideh Firoozbakht, Jan 07 2015

@[category research open, AMS 11]
theorem conjecture3 :
    answer(sorry) =
      if h : ∃ p, p.Prime ∧ 2 < p ∧ ((10 ^ (p ^ 2) - 1) / (10 ^ p - 1)).Prime then
        some (sInf {p | p.Prime ∧ 2 < p ∧ ((10 ^ (p ^ 2) - 1) / (10 ^ p - 1)).Prime})
      else
        none := by⊢ sorry =
  if h : ∃ p, Nat.Prime p ∧ 2 < p ∧ Nat.Prime ((10 ^ p ^ 2 - 1) / (10 ^ p - 1)) then
    some (sInf {p | Nat.Prime p ∧ 2 < p ∧ Nat.Prime ((10 ^ p ^ 2 - 1) / (10 ^ p - 1))})
  else none
  sorryAll goals completed! 🐙

end OeisA86766