From: Manuel Eberl <manuel@pruvisto.org>
Sophie Germain’s Theorem
by Benoît Ballenghien
Sophie Germain's theorem states that if p is a prime number such that
2p+1 is also prime (with p then called a Sophie Germain prime), a weak
version of Fermat’s Last Theorem (FLT) holds for the exponent p. That
is, there exist no nontrivial integer solutions x,y,z ∈ ℤ to the
equation x^p + y^p = z^p such that p divides neither x, y nor z. After
some preliminary results, mainly on sufficient criteria for FLT, we
propose a formalization of the classical version of Sophie Germain's
theorem as well as a variant involving the concept of auxiliary primes
that generalizes Sophie Germain primes.
https://www.isa-afp.org/entries/Sophie_Germain.html
Enjoy!
Manuel
Last updated: May 06 2025 at 08:28 UTC