Selfridge's conjectures

Reference: Wikipedia

structure Selfridge.IsSelfridge (p : ℕ) : Prop

A number p satisfies the Selfridge condition if

1. p is odd,
2. p ≡ ± 2 (mod 5),
3. 2^(p-1) ≡ 1 (mod p)
4. (p+1).fib ≡ 0 (mod p)

This is the condition that is tested in the PSW conjecture. Note: this is non-standard terminology.

• is_odd : Odd p
• mod_5 : p ≡ 2 [MOD 5] ∨ p ≡ 3 [MOD 5]
• pow_2 : 2 ^ (p - 1) ≡ 1 [MOD p]
• fib : Nat.fib (p + 1) ≡ 0 [MOD p]

theorem Selfridge.isSelfridge_iff (p : ℕ) : IsSelfridge p ↔ Odd p ∧ (p ≡ 2 [MOD 5] ∨ p ≡ 3 [MOD 5]) ∧ 2 ^ (p - 1) ≡ 1 [MOD p] ∧ Nat.fib (p + 1) ≡ 0 [MOD p]

structure Selfridge.IsPseudoSelfridge (p : ℕ) : Prop

A number p satisfies the Pseudo Selfridge condition if

1. p is odd,
2. p ≡ ± 1 (mod 5),
3. 2^(p-1) ≡ 1 (mod p)
4. (p-1).fib ≡ 0 (mod p)

This is a variant of the condition that is tested in the PSW conjecture, and appears in the wiki page mentioned above.

Note: this is non-standard terminology.

• is_odd : Odd p
• mod_5 : p ≡ 1 [MOD 5] ∨ p ≡ 4 [MOD 5]
• pow_2 : 2 ^ (p - 1) ≡ 1 [MOD p]
• fib : Nat.fib (p - 1) ≡ 0 [MOD p]

theorem Selfridge.isPseudoSelfridge_iff (p : ℕ) : IsPseudoSelfridge p ↔ Odd p ∧ (p ≡ 1 [MOD 5] ∨ p ≡ 4 [MOD 5]) ∧ 2 ^ (p - 1) ≡ 1 [MOD p] ∧ Nat.fib (p - 1) ≡ 0 [MOD p]

theorem Selfridge.selfridge_conjecture (p : ℕ) (hp : IsSelfridge p) : Nat.Prime p

PSW conjecture (Selfridge's test) Let $p$ be an odd number, with $p \equiv \pm 2 \pmod{5}$, $2^{p-1} \equiv 1 \pmod{p}$ and $F_{p+1} \equiv 0 \pmod{p}$, then $p$ is a prime number.

theorem Selfridge.selfridge_conjecture.variants.exist_pseudo_counterexample : ∃ (n : ℕ), IsPseudoSelfridge n ∧ ¬Nat.Prime n

Selfridge's test variant: Let $p$ be an odd number, with $p \equiv \pm 1 \pmod{5}$, $2^{p-1} \equiv 1 \pmod{p}$ and $F_{p-1} \equiv 0 \pmod{p}$, then $p$ is a prime number.

This test does not work.

theorem Selfridge.selfridge_conjecture.variants.pseudo_counterexample : IsPseudoSelfridge 6601 ∧ ¬Nat.Prime 6601 ∧ 6601 ≡ 1 [MOD 5]

Selfridge's test variant: Let $p$ be an odd number, with $p \equiv \pm 1 \pmod{5}$, $2^{p-1} \equiv 1 \pmod{p}$ and $F_{p-1} \equiv 0 \pmod{p}$, then $p$ is a prime number.

The number $6601$ is a conterexample to this test satisfying $6601 ≡ 1 \mod 5$

theorem Selfridge.selfridge_conjecture.variants.pseudo_counterexample' : IsPseudoSelfridge 30889 ∧ ¬Nat.Prime 30889 ∧ 30889 ≡ 3 [MOD 5]

Selfridge's test variant: Let $p$ be an odd number, with $p \equiv \pm 1 \pmod{5}$, $2^{p-1} \equiv 1 \pmod{p}$ and $F_{p-1} \equiv 0 \pmod{p}$, then $p$ is a prime number.

The number $30889$ is a conterexample to this test satisfying $30889 ≡ - 1 \mod 5$

Selfridge's conjectures about Fermat numbers

def Selfridge.fermatFactors (n : ℕ) : ℕ

OEIS A046052 The number of distinct prime factors of nth Fermat number. Known terms: 1, 1, 1, 1, 1, 2, 2, 2, 2, 3, 4, 5

Equations

• Selfridge.fermatFactors n = n.fermatNumber.primeFactors.card

theorem Selfridge.selfridge_seq_conjecture : ¬Monotone fermatFactors

Selfridge conjectured that the number of prime factors of the n-th Fermat number does not grow monotonically in $n$.

theorem Selfridge.selfridge_seq_conjecture.variants.sufficient_condition (n : ℕ) (hn : Prime n.fermatNumber) (hn' : n ≥ 5) : ¬Monotone fermatFactors

Selfridge conjectured that the number of prime factors of the n-th Fermat number does not grow monotonically in $n$.

A sufficient condition for this conjecture to hold is that there exists a Fermat prime larger than 65537.