English
F_n is prime if 3^{2^{2^n-1}} ≡ -1 (mod F_n) (Pépin's test).
Русский
Число Ферма F_n простое, если 3^{2^{2^n-1}} ≡ -1 (mod F_n) (тест Пепина).
LaTeX
$$Pépin's test:\\( 3^{2^{2^n-1}} \\equiv -1 \\pmod{\\mathrm{fermatNumber}(n)} \\Rightarrow \\mathrm{fermatNumber}(n) \\text{ is prime}$$
Lean4
/-- `Fₙ = 2^(2^n)+1` is prime if `3^(2^(2^n-1)) = -1 mod Fₙ` (**Pépin's test**). -/
theorem pepin_primality (n : ℕ) (h : 3 ^ (2 ^ (2 ^ n - 1)) = (-1 : ZMod (fermatNumber n))) : (fermatNumber n).Prime :=
by
have := Fact.mk (two_lt_fermatNumber n)
have key : 2 ^ n = 2 ^ n - 1 + 1 := (Nat.sub_add_cancel Nat.one_le_two_pow).symm
apply lucas_primality (p := 2 ^ (2 ^ n) + 1) (a := 3)
· rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
· intro p hp1 hp2
rw [Nat.add_sub_cancel, (Nat.prime_dvd_prime_iff_eq hp1 prime_two).mp (hp1.dvd_of_dvd_pow hp2), key, pow_succ,
Nat.mul_div_cancel _ two_pos, ← pow_succ, ← key, h]
exact neg_one_ne_one
