Sophie Germain primes

DefinitionSophie Germain primes#✓fully proved

A natural number \(p\) is a Sophie Germain prime if \(p\) is prime and \(2p + 1\) is prime. The case \(p = 2\) is not excluded.

def IsSophieGermainPrime (p : ℕ) : Prop :=
  Nat.Prime p ∧ Nat.Prime (2 * p + 1)

Sources

• arXiv:2311.13375, lines 83–85.

Used by 7

Used byFermat-type characterizations of Sophie Germain primes · Infinitely many primes are not Sophie Germain primes · Characterization of Sophie Germain primes · Wilson-type characterization of Sophie Germain primes · Sophie Germain primes are prime · Safe prime of a Sophie Germain prime · Primes that are not Sophie Germain primes

TheoremCharacterization of Sophie Germain primes#✓fully proved

A natural number \(p\) is a Sophie Germain prime if and only if \(p\) is prime and \(2p + 1\) is prime.

theorem isSophieGermainPrime_iff (p : ℕ) :
    IsSophieGermainPrime p ↔ Nat.Prime p ∧ Nat.Prime (2 * p + 1)

Uses 1

Statement usesSophie Germain primes

TheoremSophie Germain primes are prime#✓fully proved

If \(p\) is a Sophie Germain prime, then \(p\) is prime.

theorem IsSophieGermainPrime.prime {p : ℕ} (h : IsSophieGermainPrime p) :
    Nat.Prime p

Uses 1

Statement usesSophie Germain primes

TheoremSafe prime of a Sophie Germain prime#✓fully proved

If \(p\) is a Sophie Germain prime, then \(2p + 1\) is prime.

theorem IsSophieGermainPrime.prime_two_mul_add_one {p : ℕ} (h : IsSophieGermainPrime p) :
    Nat.Prime (2 * p + 1)

Uses 1

Statement usesSophie Germain primes

TheoremInfinitely many primes are not Sophie Germain primes#●ready to prove

The set of primes \(q\) that are not Sophie Germain primes, that is, the primes \(q\) for which \(2q + 1\) is not prime, is infinite.

public theorem_wanted infinite_setOf_prime_not_isSophieGermainPrime :
    {q : ℕ | q.Prime ∧ ¬ q.IsSophieGermainPrime}.Infinite

Sources

• Takashi Agoh, A Note on Sophie Germain Primes, INTEGERS 25 (2025), Article A83, Theorem 3.1.

Uses 1

Statement usesSophie Germain primes

TheoremPrimes that are not Sophie Germain primes#●ready to prove

For an odd prime \(p\), let \(A(p) = \{pr + (p - 1)/2 : r = 1, 2, 3, \dots\}\), and let \(A\) be the union of the sets \(A(p)\) over all odd primes \(p\). A prime is not a Sophie Germain prime if and only if it lies in \(A\); equivalently, the Sophie Germain primes are exactly the primes outside \(A\).

public theorem_wanted setOf_prime_not_isSophieGermainPrime_eq_inter :
    {q : ℕ | q.Prime ∧ ¬ q.IsSophieGermainPrime} =
      {q : ℕ | q.Prime} ∩
        {q : ℕ | ∃ p r : ℕ, p.Prime ∧ p ≠ 2 ∧ 1 ≤ r ∧ q = p * r + (p - 1) / 2}

Sources

• Takashi Agoh, A Note on Sophie Germain Primes, INTEGERS 25 (2025), Article A83, Theorem 2.1.

Uses 1

Statement usesSophie Germain primes

TheoremWilson-type characterization of Sophie Germain primes#●ready to prove

Let \(a \ge 2\) be a natural number. Then \(a\) is a Sophie Germain prime other than \(2\) if and only if \((a - 1)! \equiv 2a - 1 \pmod{a(2a + 1)}\) or \((a - 1)! \equiv -(6a + 1) \pmod{a(2a + 1)}\), the congruences being taken in the integers.

The paper states this for all positive integers \(a\); at \(a = 1\) the first congruence holds (\(0! = 1 \equiv 1 \pmod 3\)) while \(1\) is not prime (the proof's appeal to Wilson's theorem modulo \(a\) needs \(a \ge 2\)).

public theorem_wanted isSophieGermainPrime_ne_two_iff_factorial_modEq {a : ℕ} (ha : 2 ≤ a) :
    (a.IsSophieGermainPrime ∧ a ≠ 2) ↔
      ((a - 1).factorial : ℤ) ≡ 2 * a - 1 [ZMOD a * (2 * a + 1)] ∨
        ((a - 1).factorial : ℤ) ≡ -(6 * a + 1) [ZMOD a * (2 * a + 1)]

Sources

• Takashi Agoh, A Note on Sophie Germain Primes, INTEGERS 25 (2025), Article A83, Theorem 5.3.

Uses 1

Statement usesSophie Germain primes

4 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.