FormalConjectures.Wikipedia.Selfridge

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Selfridge's conjectures

Reference: Wikipedia


namespace Selfridge


section PrimalityTesting

A number p satisfies the Selfridge condition if

p is odd,

p ≡ ± 2 (mod 5),

2^(p-1) ≡ 1 (mod p)

(p+1).fib ≡ 0 (mod p)

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

@[mk_iff]
structure IsSelfridge (p : ℕ) where
  is_odd : Odd p
  mod_5 : p ≡ 2 [MOD 5] ∨ p ≡ 3 [MOD 5]
  pow_2 : 2^(p-1) ≡ 1 [MOD p]
  fib : (p+1).fib ≡ 0 [MOD p]

A number p satisfies the Pseudo Selfridge condition if

p is odd,

p ≡ ± 1 (mod 5),

2^(p-1) ≡ 1 (mod p)

(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.

@[mk_iff]
structure IsPseudoSelfridge (p : ℕ) where
  is_odd : Odd p
  mod_5 : p ≡ 1 [MOD 5] ∨ p ≡ 4 [MOD 5]
  pow_2 : 2^(p-1) ≡ 1 [MOD p]
  fib : (p-1).fib ≡ 0 [MOD 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.

@[category research open, AMS 11]
theorem declaration uses 'sorry'selfridge_conjecture (p : ℕ) (hp : IsSelfridge p) : p.Prime := byp:ℕhp:IsSelfridge p⊢ Nat.Prime p
  sorryAll goals completed! 🐙

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.

@[category textbook, AMS 11]
theorem selfridge_conjecture.variants.exist_pseudo_counterexample :
    ∃ n : ℕ, IsPseudoSelfridge n ∧ ¬ n.Prime := by⊢ ∃ n, IsPseudoSelfridge n ∧ ¬Nat.Prime n
  use 6601h⊢ IsPseudoSelfridge 6601 ∧ ¬Nat.Prime 6601
  refine ⟨⟨?_, ?_, ?_, ?_⟩, ?_⟩h.refine_1⊢ Odd 6601h.refine_2⊢ 6601 ≡ 1 [MOD 5] ∨ 6601 ≡ 4 [MOD 5]h.refine_3⊢ 2 ^ (6601 - 1) ≡ 1 [MOD 6601]h.refine_4⊢ Nat.fib (6601 - 1) ≡ 0 [MOD 6601]h.refine_5⊢ ¬Nat.Prime 6601 <;>h.refine_1⊢ Odd 6601h.refine_2⊢ 6601 ≡ 1 [MOD 5] ∨ 6601 ≡ 4 [MOD 5]h.refine_3⊢ 2 ^ (6601 - 1) ≡ 1 [MOD 6601]h.refine_4⊢ Nat.fib (6601 - 1) ≡ 0 [MOD 6601]h.refine_5⊢ ¬Nat.Prime 6601 decide +nativeAll goals completed! 🐙

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$

@[category textbook, AMS 11]
theorem selfridge_conjecture.variants.pseudo_counterexample :
    IsPseudoSelfridge 6601 ∧ ¬ (6601).Prime ∧ 6601 ≡ 1 [MOD 5] := by⊢ IsPseudoSelfridge 6601 ∧ ¬Nat.Prime 6601 ∧ 6601 ≡ 1 [MOD 5]
  refine ⟨⟨?_, ?_, ?_, ?_⟩, ?_, ?_⟩refine_1⊢ Odd 6601refine_2⊢ 6601 ≡ 1 [MOD 5] ∨ 6601 ≡ 4 [MOD 5]refine_3⊢ 2 ^ (6601 - 1) ≡ 1 [MOD 6601]refine_4⊢ Nat.fib (6601 - 1) ≡ 0 [MOD 6601]refine_5⊢ ¬Nat.Prime 6601refine_6⊢ 6601 ≡ 1 [MOD 5] <;>refine_1⊢ Odd 6601refine_2⊢ 6601 ≡ 1 [MOD 5] ∨ 6601 ≡ 4 [MOD 5]refine_3⊢ 2 ^ (6601 - 1) ≡ 1 [MOD 6601]refine_4⊢ Nat.fib (6601 - 1) ≡ 0 [MOD 6601]refine_5⊢ ¬Nat.Prime 6601refine_6⊢ 6601 ≡ 1 [MOD 5] decide +nativeAll goals completed! 🐙

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$

@[category textbook, AMS 11]
theorem selfridge_conjecture.variants.pseudo_counterexample' :
    IsPseudoSelfridge 30889 ∧ ¬ (30889).Prime ∧ 30889 ≡ 4 [MOD 5] := by⊢ IsPseudoSelfridge 30889 ∧ ¬Nat.Prime 30889 ∧ 30889 ≡ 4 [MOD 5]
  refine ⟨⟨?_, ?_, ?_, ?_⟩, ?_, ?_⟩refine_1⊢ Odd 30889refine_2⊢ 30889 ≡ 1 [MOD 5] ∨ 30889 ≡ 4 [MOD 5]refine_3⊢ 2 ^ (30889 - 1) ≡ 1 [MOD 30889]refine_4⊢ Nat.fib (30889 - 1) ≡ 0 [MOD 30889]refine_5⊢ ¬Nat.Prime 30889refine_6⊢ 30889 ≡ 4 [MOD 5] <;>refine_1⊢ Odd 30889refine_2⊢ 30889 ≡ 1 [MOD 5] ∨ 30889 ≡ 4 [MOD 5]refine_3⊢ 2 ^ (30889 - 1) ≡ 1 [MOD 30889]refine_4⊢ Nat.fib (30889 - 1) ≡ 0 [MOD 30889]refine_5⊢ ¬Nat.Prime 30889refine_6⊢ 30889 ≡ 4 [MOD 5] decide +nativeAll goals completed! 🐙


end PrimalityTesting


section FermatNumbers

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

def fermatFactors (n : ℕ) : ℕ := n.fermatNumber.primeFactors.card

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

@[category research open, AMS 11]
theorem declaration uses 'sorry'selfridge_seq_conjecture : ¬ Monotone fermatFactors := by⊢ ¬Monotone fermatFactors
  sorryAll goals completed! 🐙

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.

@[category research solved, AMS 11]
theorem selfridge_seq_conjecture.variants.sufficient_condition (n : ℕ) (hn : Prime n.fermatNumber)
    (hn' : n ≥ 5) : type_of% selfridge_seq_conjecture := byn:ℕhn:Prime n.fermatNumberhn':n ≥ 5⊢ ¬Monotone fermatFactors
  intro hmonon:ℕhn:Prime n.fermatNumberhn':n ≥ 5hmono:Monotone fermatFactors⊢ False
  have hp : (n.fermatNumber).Prime := hn.nat_primen:ℕhn:Prime n.fermatNumberhn':n ≥ 5hmono:Monotone fermatFactorshp:Nat.Prime n.fermatNumber := Prime.nat_prime hn⊢ False
  have h1 : fermatFactors n = 1 := byn:ℕhn:Prime n.fermatNumberhn':n ≥ 5⊢ ¬Monotone fermatFactors
    unfold fermatFactorsn:ℕhn:Prime n.fermatNumberhn':n ≥ 5hmono:Monotone fermatFactorshp:Nat.Prime n.fermatNumber := Prime.nat_prime hn⊢ n.fermatNumber.primeFactors.card = 1
    rw [hp.primeFactors, Finset.card_singleton]All goals completed! 🐙
  have h5 : fermatFactors 5 = 2 := byn:ℕhn:Prime n.fermatNumberhn':n ≥ 5⊢ ¬Monotone fermatFactors native_decideAll goals completed! 🐙
  have hle := hmono hn'n:ℕhn:Prime n.fermatNumberhn':n ≥ 5hmono:Monotone fermatFactorshp:Nat.Prime n.fermatNumber := Prime.nat_prime hnh1:fermatFactors n = 1 := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a.card = 1) (Nat.Prime.primeFactors hp)))
      (Eq.mpr (id (congrArg (fun _a => _a = 1) (Finset.card_singleton n.fermatNumber))) (Eq.refl 1)))h5:fermatFactors 5 = 2 := sufficient_condition._proof_1hle:fermatFactors 5 ≤ fermatFactors n := hmono hn'⊢ False
  rw [h1, h5] at hlen:ℕhn:Prime n.fermatNumberhn':n ≥ 5hmono:Monotone fermatFactorshp:Nat.Prime n.fermatNumber := Prime.nat_prime hnh1:fermatFactors n = 1 := 
  id
    (Eq.mpr (id (congrArg (fun _a => _a.card = 1) (Nat.Prime.primeFactors hp)))
      (Eq.mpr (id (congrArg (fun _a => _a = 1) (Finset.card_singleton n.fermatNumber))) (Eq.refl 1)))h5:fermatFactors 5 = 2 := sufficient_condition._proof_1hle:2 ≤ 1⊢ False
  omegaAll goals completed! 🐙


end FermatNumbers


end Selfridge