/-
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
open Filter Topology Realnamespace OeisA38771$a(n)$ is the smallest composite number $c$ such that $\textrm{primorial}(n) + c$ is prime.
noncomputable def a (n : ℕ) : ℕ :=
let Qn : ℕ := ∏ i ∈ Finset.range n, Nat.nth Nat.Prime i
let is_composite (c : ℕ) : Prop := c > 1 ∧ ¬ c.Prime
sInf { c : ℕ | is_composite c ∧ (Qn + c).Prime }hQ:∏ i ∈ Finset.range 0, Nat.nth Nat.Prime i = 1h_least:IsLeast {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (1 + c)} 4⊢ sInf {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (1 + c)} = 4
All goals completed! 🐙hQ:∏ i ∈ Finset.range 1, Nat.nth Nat.Prime i = 2h_least:IsLeast {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (2 + c)} 9⊢ sInf {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (2 + c)} = 9
All goals completed! 🐙hQ:∏ i ∈ Finset.range 2, Nat.nth Nat.Prime i = 6h_least:IsLeast {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (6 + c)} 25⊢ sInf {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (6 + c)} = 25
All goals completed! 🐙hQ:∏ i ∈ Finset.range 3, Nat.nth Nat.Prime i = 30h_least:IsLeast {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (30 + c)} 49⊢ sInf {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (30 + c)} = 49
All goals completed! 🐙$a(n) \ne 0$ for all $n$ (i.e., a suitable composite $c$ always exists). The following more general statement follows from Dirichlet's theorem on primes in arithmetic progressions: there doesn't exist a > 0 natural number such that p - a is prime for every prime p > a.
Choose q prime such that q is coprime with a, and p > a + q prime such that q | p - a (such a p exists from Dirichlet's theorem). Then p - a is composite, a contradiction.
@[category textbook, AMS 11]
theorem a_n_exists (n : ℕ) : a n ≠ 0 := n:ℕ⊢ a n ≠ 0
All goals completed! 🐙Conjecture: $\liminf_{n \to \infty} \frac{a(n)}{p_{n+1}^2} = 1 <$ $\limsup_{n \to \infty} \frac{a(n)}{p_{n+1}^2} = 2$.
Charles R Greathouse IV and Thomas Ordowski, Apr 24 2015
@[category research open, AMS 11]
theorem conjecture1 :
let p_next_sq (n : ℕ) : ℝ := ((Nat.nth Nat.Prime n : ℝ)) ^ 2
let seq (n : ℕ) : ℝ := (a n : ℝ) / p_next_sq n
(liminf seq atTop = 1) ∧ (limsup seq atTop = 2) := ⊢ let p_next_sq := fun n ↦ ↑(Nat.nth Nat.Prime n) ^ 2;
let seq := fun n ↦ ↑(a n) / p_next_sq n;
liminf seq atTop = 1 ∧ limsup seq atTop = 2
All goals completed! 🐙All the terms in this sequence have exactly two prime factors. This conjecture is true for the first 133 terms.
Dmitry Kamenetsky, Jan 06 2019
@[category research open, AMS 11]
theorem conjecture2 (n : ℕ) : (a n).IsSemiprime := n:ℕ⊢ (a n).IsSemiprime
All goals completed! 🐙end OeisA38771