Selfridge.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 2 contain sorry, 0 declared as axioms

Selfridge's conjectures

Reference: Wikipedia

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

structure Selfridge.IsSelfridge A number p satisfies the Selfridge condition if 1 line 43 source
Source documentation
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.
standard axioms: propext what this means
Statement uses: Nat
```
structure IsSelfridge (p : ℕ) where
…
```
structure Selfridge.IsPseudoSelfridge A number p satisfies the Pseudo Selfridge condition if 1 line 61 source
Source documentation
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.
standard axioms: propext what this means
Statement uses: Nat
```
structure IsPseudoSelfridge (p : ℕ) where
…
```
theorem Selfridge.selfridge_conjecture 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 sorry line 73 source
Source documentation
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.

depends on sorry what this means
Statement uses: Nat, Selfridge.IsSelfridge, Nat.Prime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem selfridge_conjecture (p : ℕ) (hp : IsSelfridge p) : p.Prime := by
…
```
Mentions: Selfridge.IsSelfridge
theorem Selfridge.selfridge_conjecture.variants.exist_pseudo_counterexample 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 line 84 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Nat, And, GT.gt, OfNat.ofNat, Selfridge.IsPseudoSelfridge, Not, Nat.Prime
Proof uses: Exists.intro, And.intro, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.false, Selfridge.IsPseudoSelfridge.mk, Iff.mp, Eq, HMod.hMod, Bool.rec, Odd, Bool.true, Iff.symm, Nat.odd_iff, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natMod, of_eq_true, Or and 36 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem selfridge_conjecture.variants.exist_pseudo_counterexample :
    ∃ n > 1, IsPseudoSelfridge n ∧ ¬ n.Prime := by
…
```
Mentions: Selfridge.IsPseudoSelfridge
theorem Selfridge.selfridge_conjecture.variants.pseudo_counterexample 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 line 98 source
Source documentation
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$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Selfridge.IsPseudoSelfridge, OfNat.ofNat, Nat, Not, Nat.Prime, Nat.ModEq
Proof uses: And.intro, Selfridge.IsPseudoSelfridge.mk, Iff.mp, Eq, HMod.hMod, Bool.rec, Bool, Odd, Bool.true, Iff.symm, Nat.odd_iff, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, of_eq_true, Or, Eq.trans, True, False and 33 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem selfridge_conjecture.variants.pseudo_counterexample :
    IsPseudoSelfridge 6601 ∧ ¬ (6601).Prime ∧ 6601 ≡ 1 [MOD 5] := by
…
```
Mentions: Selfridge.IsPseudoSelfridge
theorem Selfridge.selfridge_conjecture.variants.pseudo_counterexample' 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 line 111 source
Source documentation
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$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, Selfridge.IsPseudoSelfridge, OfNat.ofNat, Nat, Not, Nat.Prime, Nat.ModEq
Proof uses: And.intro, Selfridge.IsPseudoSelfridge.mk, Iff.mp, Eq, HMod.hMod, Bool.rec, Bool, Odd, Bool.true, Iff.symm, Nat.odd_iff, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_natMod, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, of_eq_true, Or, Eq.trans, True, False and 33 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem selfridge_conjecture.variants.pseudo_counterexample' :
    IsPseudoSelfridge 30889 ∧ ¬ (30889).Prime ∧ 30889 ≡ 4 [MOD 5] := by
…
```
Mentions: Selfridge.IsPseudoSelfridge
def Selfridge.fermatFactors OEIS A46052 The number of distinct prime factors of nth Fermat number line 129 source
Source documentation
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

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.card, Nat.primeFactors, Nat.fermatNumber
```
def fermatFactors (n : ℕ) : ℕ := n.fermatNumber.primeFactors.card
…
```
theorem Selfridge.selfridge_seq_conjecture Selfridge conjectured that the number of prime factors of the n-th Fermat number does not grow monotonically in $n$ sorry line 136 source
Source documentation
Selfridge conjectured that the number of prime factors of the n-th Fermat number does not grow monotonically in $n$.

depends on sorry what this means
Statement uses: Not, Monotone, Nat, Selfridge.fermatFactors
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem selfridge_seq_conjecture : ¬ Monotone fermatFactors := by
…
```
Mentions: Selfridge.fermatFactors
theorem Selfridge.selfridge_seq_conjecture.variants.sufficient_condition Selfridge conjectured that the number of prime factors of the n-th Fermat number does not grow monotonically in $n$ line 147 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Prime, Nat.fermatNumber, GE.ge, OfNat.ofNat, Not, Monotone, Selfridge.fermatFactors
Proof uses: Eq, of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.card, Nat.primeFactors, Singleton.singleton, Finset, Nat.Prime.primeFactors, Prime.nat_prime, Finset.card_singleton, eq_self, HMul.hMul, congr, Mathlib.Meta.NormNum.IsNat.to_eq, HAdd.hAdd, HPow.hPow, Mathlib.Meta.NormNum.isNat_add and 35 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem selfridge_seq_conjecture.variants.sufficient_condition (n : ℕ) (hn : Prime n.fermatNumber)
    (hn' : n ≥ 5) : type_of% selfridge_seq_conjecture := by
…
```
Mentions: Selfridge.selfridge_seq_conjecture