Special classes of primes

Fermat, Mersenne, Sophie Germain, Wieferich, Cullen and other named prime families, Fermat numbers, Sierpiński–Riesel numbers, prime-producing formulas.

DefinitionFortunate numbers#✓fully proved

Write \(q\#\) for the primorial of a natural number \(q\), the product of all primes \(p \le q\). For natural numbers \(q\) and \(m\), \(m\) is the Fortunate number of \(q\) when \(q\) is prime, \(m > 1\), \(q\# + m\) is prime, and \(q\# + k\) is not prime for any \(k\) with \(1 < k < m\).

def IsFortunateNumber (q m : ℕ) : Prop :=
  q.Prime ∧ 1 < m ∧ (primorial q + m).Prime ∧
    ∀ k, 1 < k → k < m → ¬ (primorial q + k).Prime
Sources
  • Antonín Čejchan, Michal Křížek, and Lawrence Somer, On Remarkable Properties of Primes Near Factorials and Primorials, Journal of Integer Sequences 25 (2022), Article 22.1.4.

TheoremGandhi's formula for the \(n\)th prime#✓fully proved

For \(i \ge 1\) let \(p_i\) be the \(i\)th prime, so that \(p_1 = 2\), and for \(n \ge 1\) let \(P_{n-1} = p_1 p_2 \cdots p_{n-1}\), the empty product \(1\) when \(n = 1\). Let \(\mu\) be the Möbius function. Then for every \(n \ge 1\),

\[p_n = \left\lfloor 1 - \log_2 \left( -\frac{1}{2} + \sum_{d \mid P_{n-1}} \frac{\mu(d)}{2^d - 1} \right) \right\rfloor.\]
theorem gandhi_nthPrimeFormula (n : ℕ) (hn : 0 < n) :
    ((Nat.nth Nat.Prime (n - 1) : ℕ) : ℤ) =
      ⌊1 - Real.logb 2 (-1 / 2 +
        ∑ d ∈ Nat.divisors
          (∏ i ∈ Finset.Icc 1 (n - 1), Nat.nth Nat.Prime (i - 1)),
          (((ArithmeticFunction.moebius d : ℤ) : ℝ) / ((2 : ℝ) ^ d - 1)))⌋
Sources
  • J. M. Gandhi, "Formulae for the nth prime," Proc. Washington State University Conference on Number Theory (1971), 96--107. The displayed formula and indexing follow the secondary source Eric S. Rowland, "A Natural Prime-Generating Recurrence," Journal of Integer Sequences 11 (2008), Article 08.2.8, lines 90--103 of the official TeX, https://cs.uwaterloo.ca/journals/JIS/VOL11/Rowland/rowland21.tex, where f(n) is the nth prime pₙ and Pₙ = p₁ p₂ ⋯ pₙ.

DefinitionGeneralized Fermat number#✓fully proved

For an even natural number \(b\) and a positive integer \(n\), the generalized Fermat number is \(F_n(b) = b^{2^n} + 1\) (also written \(F_{b,n}\)).

def generalizedFermatNumber (b n : ℕ) (_hb : Even b) (_hn : 0 < n) : ℕ :=
  b ^ (2 ^ n) + 1
Sources
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.