Primality tests and pseudoprimes

Primality criteria (Proth, Pocklington, Lucas–Lehmer), Fermat, Lucas, Frobenius and strong pseudoprimes, Carmichael and Korselt numbers.

• Absolute Lucas pseudoprimes
• Carmichael index
• Carmichael numbers
• Even pseudoprimes
• Fermat congruence criteria for twin and Sophie Germain primes
• Fermat pseudoprimes
• Frobenius pseudoprimes
• Generalized Carmichael numbers
• Lucas–Lehmer test
• Strong pseudoprimes

TheoremInfinitely many Fibonacci pseudoprimes at twice-prime indices#✓fully proved

Let \(F_m\) denote the \(m\)-th Fibonacci number. There are infinitely many primes \(p\) such that \(n = F_{2p}\) satisfies \(n > 1\), \(n\) is not prime, and \(n\) divides \(F_{n - \left(\frac{5}{n}\right)}\), where \(\left(\frac{5}{n}\right)\) is the Jacobi symbol. In other words, \(F_{2p}\) is a Fibonacci pseudoprime: a composite number \(n\) that divides \(F_{n - \left(\frac{5}{n}\right)}\).

theorem infinitely_many_primes_fibonacci_pseudoprime :
    Set.Infinite {p : ℕ | p.Prime ∧
      let n := Nat.fib (2 * p)
      n ∣ Nat.fib (Int.toNat ((n : ℤ) - jacobiSym 5 n)) ∧ ¬n.Prime ∧ 1 < n}

Sources

• Y. Hamahata and Y. Kokubun, "Cipolla Pseudoprimes," Journal of Integer Sequences 10 (2007), Article 07.8.6, Corollary 4 [Lehmer], lines 321–324 (Fibonacci-pseudoprime definition at lines 313–318), https://cs.uwaterloo.ca/journals/JIS/VOL10/Hamahata2/hamahata44.tex

TheoremPocklington's criterion for \(N = Kp^e + 1\)#✓fully proved

Let \(N\), \(K\) and \(e\) be natural numbers and let \(p\) be a prime, with \(0 < K < p^e\) and \(N = Kp^e + 1\). If some natural number \(a\) satisfies \(a^{N-1} \equiv 1 \pmod{N}\) and \(\gcd\big(a^{(N-1)/p} - 1, N\big) = 1\), where \((N-1)/p\) is the quotient of \(N - 1\) by \(p\) rounded down and \(a^{(N-1)/p} - 1\) is truncated at \(0\), then \(N\) is prime.

Proof: The proof follows Pocklington's standard least-prime-factor order argument, from Pocklington (1914) as stated by Grau and Oller-Marcen, arXiv:1011.4836v3, lines 60-69.

public theorem pocklington_prime_power_criterion (N K p e : ℕ)
    (hKpos : 0 < K) (hp : Nat.Prime p)
    (hN : N = K * p ^ e + 1) (hlt : K < p ^ e)
    (hex : ∃ a : ℕ, Nat.ModEq N (a ^ (N - 1)) 1 ∧
      Nat.gcd (a ^ ((N - 1) / p) - 1) N = 1) :
    Nat.Prime N

Sources

• Pocklington (1914), as stated in Grau and Oller-Marcen, "A primality test for Kp^n+1 numbers", arXiv:1011.4836v3, lines 60-69, which give the complete condition, including gcd(a^((N-1)/p)-1,N)=1. The source's integer witness a ∈ ℤ is represented here by a natural residue representative a : ℕ, using Nat.ModEq and Nat.gcd with natural subtraction in the exponents.

TheoremProth's theorem#✓fully proved

Let \(h\) and \(k\) be natural numbers with \(h\) odd and \(h < 2^k\), and let \(N = h \cdot 2^k + 1\). Then \(N\) is prime if and only if there is a residue class \(a\) modulo \(N\) with \(a^{(N-1)/2} = -1\) in \(\mathbb{Z}/N\mathbb{Z}\).

Proof: The forward implication uses a nonsquare and Euler's criterion; the reverse uses Proth's least-prime-factor order argument. Sources: Proth (1878), p. 926, and the Wikipedia exposition.

theorem proth_theorem (h k N : ℕ) (hOdd : Odd h) (hlt : h < 2 ^ k)
    (hN : N = h * 2 ^ k + 1) :
    Nat.Prime N ↔ ∃ a : ZMod N, a ^ ((N - 1) / 2) = -1

Sources

• https://en.wikipedia.org/wiki/Proth%27s_theorem

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.