jacobsthal_function_conjecture
Provedanalysisgraph-theorynumber-theory
Jacobsthal function g(pₙ#): For the primorial pₙ# = 2·3·5·...·pₙ, g(pₙ#) is the maximum gap between consecutive integers coprime to pₙ#. Conjectured: g(pₙ#) ≤ pₙ₊₁². Best known: g(pₙ#) = O(pₙ log² pₙ). Open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem jacobsthal_function_conjecture :
∀ n : ℕ, 1 ≤ n →
∃ (g : ℕ),
∀ k : ℕ, (∏ p ∈ (Finset.range n).filter Nat.Prime, p) ≤ k →
∃ j : ℕ, j ≤ g ∧ Nat.Coprime (∏ p ∈ (Finset.range n).filter Nat.Prime, p) (k + j) := by
sorrySource