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

Reference: A034693

noncomputable def OeisA34693.a (n : ℕ) : ℕ

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

Equations

• OeisA34693.a n = Nat.nth (fun (k : ℕ) => Nat.Prime (k * n + 1)) 0

theorem OeisA34693.zero : a 0 = 0

theorem OeisA34693.one : a 1 = 1

theorem OeisA34693.two : a 2 = 1

theorem OeisA34693.three : a 3 = 2

theorem OeisA34693.seven : a 7 = 4

theorem OeisA34693.exists_k {n : ℕ} (hn : 1 < n) : ∃ k < n, Nat.Prime (n * k + 1)

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

theorem OeisA34693.exists_k_stronger {n : ℕ} (hn : 0 < n) : ∃ (k : ℕ), ↑k < 1 + Real.nthRoot 4 ↑n ^ 3 ∧ Nat.Prime (n * k + 1)

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

theorem OeisA34693.exists_k_best_possible : ∃ n > 0, ∀ (k : ℕ), ↑k < 1 + Real.nthRoot 100 ↑n ^ 74 → ¬Nat.Prime (n * k + 1)

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

theorem OeisA34693.a_isBigO : (fun (n : ℕ) => ↑(a n)) ≪ fun (n : ℕ) => Real.log ↑n * Real.log (Real.log ↑n)

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

theorem OeisA34693.a_unbounded : ¬BddAbove (Set.range fun (n : ℕ) => ↑(a n) / (Real.log ↑n * Real.log (Real.log ↑n)))

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