1. FormalConjectures
  2. OEIS
  3. «38771»
/- 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. -/ module public import FormalConjecturesUtil

Smallest composite $c$ such that $\textrm{primorial}(n) + c$ is prime

References:

@[expose] public sectionopen 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.

n:ℕQ:ℕ := ∏ i ∈ Finset.range n, Nat.nth Nat.Prime ihQdef:Q = ∏ i ∈ Finset.range n, Nat.nth Nat.Prime ihQ:0 < Qq:ℕhqQ:Q + 1 ≤ qhq:Nat.Prime qthis✝:NeZero qhunit:IsUnit ↑Qp:ℕhp:p > Q + qhpp:Nat.Prime phpq:↑p = ↑Qhdvd:q ∣ p - Qhmem:p - Q ∈ {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (Q + c)}this:0 ∈ {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (Q + c)}h0:(have Qn := Q; have is_composite := fun c ↦ c > 1 ∧ ¬Nat.Prime c; sInf {c | is_composite c ∧ Nat.Prime (Qn + c)}) = 0⊢ False; exact absurd this.1.1 (n:ℕQ:ℕ := ∏ i ∈ Finset.range n, Nat.nth Nat.Prime ihQdef:Q = ∏ i ∈ Finset.range n, Nat.nth Nat.Prime ihQ:0 < Qq:ℕhqQ:Q + 1 ≤ qhq:Nat.Prime qthis✝:NeZero qhunit:IsUnit ↑Qp:ℕhp:p > Q + qhpp:Nat.Prime phpq:↑p = ↑Qhdvd:q ∣ p - Qhmem:p - Q ∈ {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (Q + c)}this:0 ∈ {c | (c > 1 ∧ ¬Nat.Prime c) ∧ Nat.Prime (Q + c)}h0:(have Qn := Q; have is_composite := fun c ↦ c > 1 ∧ ¬Nat.Prime c; sInf {c | is_composite c ∧ Nat.Prime (Qn + c)}) = 0⊢ ¬0 > 1 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.

@[category research open, AMS 11] theorem conjecture2 (n : ℕ) : (a n).IsSemiprime := n:ℕ⊢ (a n).IsSemiprime All goals completed! 🐙end OeisA38771