Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Sophie Germain's Theorem


view this post on Zulip Email Gateway (May 05 2025 at 11:36):

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