Formal target: Corpus.WikipediaSelfridge.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.

Exact formal statement

∀ (p : Nat), Corpus.WikipediaSelfridge.IsSelfridge p → Nat.Prime p

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record