Abstract
Sophie Germain's theorem states that if is a prime number such that is also prime (with then called a Sophie Germain prime), a weak version of Fermat’s Last Theorem (FLT) holds for the exponent . That is, there exist no nontrivial integer solutions to the equation
such that divides neither , nor .
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.