FormalConjectures.OEIS.«34693»

/-
Copyright 2025 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 number $k$ such that $kn + 1$ is prime

References:

A34693

namespace OeisA34693open Filter

Smallest number $k$ such that $kn + 1$ is prime.

noncomputable def a (n : ℕ) : ℕ := Nat.nth (fun k ↦ (k * n + 1).Prime) 0

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

@[category test, AMS 11]
theorem a_1 : a 1 = 1 := by⊢ a 1 = 1
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k + 1).Prime) (n := 1) (by⊢ Nat.Prime (1 + 1) norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙

@[category test, AMS 11]
theorem a_2 : a 2 = 1 := by⊢ a 2 = 1
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k * 2 + 1).Prime) (n := 1) (by⊢ Nat.Prime (1 * 2 + 1) norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙

@[category test, AMS 11]
theorem a_3 : a 3 = 2 := by⊢ a 3 = 2
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k * 3 + 1).Prime) (n := 2) (by⊢ Nat.Prime (2 * 3 + 1) norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙

@[category test, AMS 11]
theorem a_7 : a 7 = 4 := by⊢ a 7 = 4
  conv_rhs => rw [← Nat.nth_count (p := fun k ↦ (k * 7 + 1).Prime) (n := 4) (by⊢ Nat.Prime (4 * 7 + 1) norm_numAll goals completed! 🐙)]
  aesop (add simp [a])All goals completed! 🐙

Conjecture: for every $n > 1$ there exists a number $k < n$ such that $nk + 1$ is a prime.

@[category research open, AMS 11]
theorem exists_k {n : ℕ} (hn : 1 < n) : ∃ k < n, (n * k + 1).Prime := byn:ℕhn:1 < n⊢ ∃ k < n, Nat.Prime (n * k + 1)
  sorryAll goals completed! 🐙

A stronger conjecture: for every n there exists a number $k < 1 + n^{0.75}$ such that $nk + 1$ is a prime.

@[category research open, AMS 11]
theorem exists_k_stronger {n : ℕ} (hn : 0 < n) : ∃ k : ℕ,
    k < 1 + (Real.nthRoot 4 n) ^ 3 ∧ (n * k + 1).Prime := byn:ℕhn:0 < n⊢ ∃ k, ↑k < 1 + Real.nthRoot 4 ↑n ^ 3 ∧ Nat.Prime (n * k + 1)
  sorryAll goals completed! 🐙

The expression $1 + n^{0.74}$ does not work as an upper bound.


@[category research solved, AMS 11]
theorem exists_k_best_possible : ∃ n > (0 : ℕ), ∀ (k : ℕ),
    k < 1 + (Real.nthRoot 100 n) ^ 74 → ¬(n * k + 1).Prime := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)
  refine ⟨19, by⊢ 19 > 0 norm_numAll goals completed! 🐙, ?_⟩
  have hy : Real.nthRoot 100 ((19 : ℕ) : ℝ) = (19 : ℝ) ^ (((100 : ℕ) : ℝ))⁻¹ := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    simp only [Real.nthRoot]⊢ (if Even 100 then ↑19 ^ (↑100)⁻¹ else ↑(SignType.sign ↑19) ^ 100 * |↑19| ^ (↑100)⁻¹) = 19 ^ (↑100)⁻¹hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    rw [if_pos (by⊢ Even 100⊢ ↑19 ^ (↑100)⁻¹ = 19 ^ (↑100)⁻¹hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) decideAll goals completed! 🐙⊢ ↑19 ^ (↑100)⁻¹ = 19 ^ (↑100)⁻¹hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) : Even 100)]⊢ ↑19 ^ (↑100)⁻¹ = 19 ^ (↑100)⁻¹hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    norm_numhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
  have h100 : (Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ (100 : ℕ) = 19 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    rw [hyhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ (19 ^ (↑100)⁻¹) ^ 100 = 19hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ (19 ^ (↑100)⁻¹) ^ 100 = 19hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)]hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ (19 ^ (↑100)⁻¹) ^ 100 = 19hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1); exact Real.rpow_inv_natCast_pow (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ 0 ≤ 19hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) norm_numAll goals completed! 🐙hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)) (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹⊢ 100 ≠ 0hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) norm_numAll goals completed! 🐙hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1))hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
  have hb : (Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ 74 ≤ 9 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    apply le_of_pow_le_pow_left₀ (n := 100) (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ 100 ≠ 0hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) norm_numAll goals completed! 🐙hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)) (byhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ 0 ≤ 9hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) norm_numAll goals completed! 🐙hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1))
    have e : ((Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ (74 : ℕ)) ^ (100 : ℕ)
        = ((Real.nthRoot 100 ((19 : ℕ) : ℝ)) ^ (100 : ℕ)) ^ (74 : ℕ) := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 74) ^ 100 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
      rw [← pow_mul,hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ Real.nthRoot 100 ↑19 ^ (74 * 100) = (Real.nthRoot 100 ↑19 ^ 100) ^ 74hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 74) ^ 100 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) ← pow_mul,hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ Real.nthRoot 100 ↑19 ^ (74 * 100) = Real.nthRoot 100 ↑19 ^ (100 * 74)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 74) ^ 100 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) Nat.mul_commhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19⊢ Real.nthRoot 100 ↑19 ^ (100 * 74) = Real.nthRoot 100 ↑19 ^ (100 * 74)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 74) ^ 100 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)]hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 74) ^ 100 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 74) ^ 100 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    rw [e,hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ (Real.nthRoot 100 ↑19 ^ 100) ^ 74 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ 19 ^ 74 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1) h100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ 19 ^ 74 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ 19 ^ 74 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)]hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19e:(Real.nthRoot 100 ↑19 ^ 74) ^ 100 = (Real.nthRoot 100 ↑19 ^ 100) ^ 74⊢ 19 ^ 74 ≤ 9 ^ 100hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
    norm_numhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9⊢ ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑19 ^ 74 → ¬Nat.Prime (19 * k + 1)
  intro k hkhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74⊢ ¬Nat.Prime (19 * k + 1)
  have hk10 : (k : ℝ) < 10 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑k < 10⊢ ¬Nat.Prime (19 * k + 1) linarithhy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑k < 10⊢ ¬Nat.Prime (19 * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑k < 10⊢ ¬Nat.Prime (19 * k + 1)
  have hk10' : k < 10 := by⊢ ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑k < 10hk10':k < 10⊢ ¬Nat.Prime (19 * k + 1) exact_mod_cast hk10hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑k < 10hk10':k < 10⊢ ¬Nat.Prime (19 * k + 1)hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑k < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑k < 10hk10':k < 10⊢ ¬Nat.Prime (19 * k + 1)
  interval_cases k«0»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑0 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑0 < 10hk10':0 < 10⊢ ¬Nat.Prime (19 * 0 + 1)«1»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑1 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑1 < 10hk10':1 < 10⊢ ¬Nat.Prime (19 * 1 + 1)«2»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑2 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑2 < 10hk10':2 < 10⊢ ¬Nat.Prime (19 * 2 + 1)«3»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑3 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑3 < 10hk10':3 < 10⊢ ¬Nat.Prime (19 * 3 + 1)«4»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑4 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑4 < 10hk10':4 < 10⊢ ¬Nat.Prime (19 * 4 + 1)«5»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑5 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑5 < 10hk10':5 < 10⊢ ¬Nat.Prime (19 * 5 + 1)«6»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑6 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑6 < 10hk10':6 < 10⊢ ¬Nat.Prime (19 * 6 + 1)«7»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑7 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑7 < 10hk10':7 < 10⊢ ¬Nat.Prime (19 * 7 + 1)«8»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑8 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑8 < 10hk10':8 < 10⊢ ¬Nat.Prime (19 * 8 + 1)«9»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑9 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑9 < 10hk10':9 < 10⊢ ¬Nat.Prime (19 * 9 + 1) <;>«0»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑0 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑0 < 10hk10':0 < 10⊢ ¬Nat.Prime (19 * 0 + 1)«1»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑1 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑1 < 10hk10':1 < 10⊢ ¬Nat.Prime (19 * 1 + 1)«2»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑2 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑2 < 10hk10':2 < 10⊢ ¬Nat.Prime (19 * 2 + 1)«3»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑3 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑3 < 10hk10':3 < 10⊢ ¬Nat.Prime (19 * 3 + 1)«4»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑4 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑4 < 10hk10':4 < 10⊢ ¬Nat.Prime (19 * 4 + 1)«5»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑5 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑5 < 10hk10':5 < 10⊢ ¬Nat.Prime (19 * 5 + 1)«6»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑6 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑6 < 10hk10':6 < 10⊢ ¬Nat.Prime (19 * 6 + 1)«7»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑7 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑7 < 10hk10':7 < 10⊢ ¬Nat.Prime (19 * 7 + 1)«8»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑8 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑8 < 10hk10':8 < 10⊢ ¬Nat.Prime (19 * 8 + 1)«9»hy:Real.nthRoot 100 ↑19 = 19 ^ (↑100)⁻¹h100:Real.nthRoot 100 ↑19 ^ 100 = 19hb:Real.nthRoot 100 ↑19 ^ 74 ≤ 9k:ℕhk:↑9 < 1 + Real.nthRoot 100 ↑19 ^ 74hk10:↑9 < 10hk10':9 < 10⊢ ¬Nat.Prime (19 * 9 + 1) norm_numAll goals completed! 🐙

Conjecture: $a(n) = O(\log(n)\log(\log(n)))$.

@[category research open, AMS 11]
theorem a_isBigO : (fun n ↦ (a n : ℝ)) =O[atTop] (fun n ↦ Real.log n * Real.log (Real.log n)) := by⊢ (fun n ↦ ↑(a n)) =O[atTop] fun n ↦ Real.log ↑n * Real.log (Real.log ↑n)
  sorryAll goals completed! 🐙

Counter-conjecture to a_isBigO: $a(n) / (\log n \log \log n)$ is unbounded.

@[category research open, AMS 11]
theorem a_unbounded : ¬BddAbove (Set.range fun n ↦ a n / (Real.log n * Real.log (Real.log n))) := by⊢ ¬BddAbove (Set.range fun n ↦ ↑(a n) / (Real.log ↑n * Real.log (Real.log ↑n)))
  sorryAll goals completed! 🐙

end OeisA34693