Fermat pseudoprimes

TheoremCipolla's pseudoprime construction#✓fully proved

Let \(a > 1\) be a natural number and let \(p\) be a prime that does not divide \(a(a^2 - 1)\). Put \(n_1 = (a^p - 1)/(a - 1)\), \(n_2 = (a^p + 1)/(a + 1)\) and \(n = n_1 n_2\). Then \(n\) is a Fermat pseudoprime to base \(a\): \(n > 1\), \(n\) is not prime, and \(n\) divides \(a^{n-1} - 1\).

theorem cipolla_pseudoprime_construction
    (a p : ℕ)
    (ha : 1 < a)
    (hp : p.Prime)
    (hnotdvd : ¬ p ∣ a * (a ^ 2 - 1)) :
    let n₁ := (a ^ p - 1) / (a - 1)
    let n₂ := (a ^ p + 1) / (a + 1)
    let n := n₁ * n₂
    Nat.FermatPsp n a
Sources

DefinitionGuy's question on non-squarefree base-two pseudoprimes beyond \(10^{13}\)#✓fully proved

The statement that there is a natural number \(n > 10^{13}\) that is a Fermat pseudoprime to base \(2\) (a composite number \(n > 1\) with \(n \mid 2^{n-1} - 1\)) and is not squarefree.

Guy reports 54 non-squarefree base-two pseudoprimes up to \(10^{13}\), all multiples of \(1093^2\) or \(3511^2\), and asks whether there are any other "square psp"s. Here "square psp" means a non-squarefree base-two pseudoprime, not a number that is itself a perfect square. Guy poses this as a question; this is its affirmative existence form, which does not predict the answer.

def conjecture : Prop :=
  ∃ n : ℕ,
    Nat.FermatPsp n 2 ∧
    ¬ Squarefree n ∧
    10 ^ 13 < n
Used by 1
Used byA non-squarefree base-two pseudoprime beyond \(10^{13}\) exists

TheoremA non-squarefree base-two pseudoprime beyond \(10^{13}\) exists#●ready to prove

There is a natural number \(n > 10^{13}\) that is a Fermat pseudoprime to base \(2\) (a composite number \(n > 1\) with \(n \mid 2^{n-1} - 1\)) and is not squarefree.

OEIS A158358 gives the witness \(n = 10063351640161 = 73 \cdot 257 \cdot 449 \cdot 1093^2\).

public theorem_wanted conjecture_holds : conjecture
Sources
  • OEIS A158358, nonsquarefree Poulet numbers, https://oeis.org/A158358.
Uses 1
Statement usesGuy's question on non-squarefree base-two pseudoprimes beyond \(10^{13}\)
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.