Sophie Germain’s Theorem

Benoît Ballenghien 📧

April 9, 2025

Abstract

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,zZ to the equation xp+yp=zp 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.

License

BSD License

Topics

Session Sophie_Germain