Theory SG_Introduction

(* Author: Benoît Ballenghien, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF *)

(*<*)
theory SG_Introduction
  imports Main
begin

context fixes n p :: nat and x y z :: int
begin

(*>*)



section ‹Introduction›

text ‹
Fermat's Last Theorem (often abbreviated to FLT) states that for any integer 
\<^term>‹2 < n›, the equation \<^term>‹x ^ n + y ^ n = z ^ n› has no nontrivial solution in the integers.
Pierre de Fermat first conjectured this result in the 17th century,
claiming to have a proof that did not fit in the margin of his notebook.
However, it remained an open problem for centuries until Andrew Wiles and Richard Taylor provided
a complete proof in 1995 using advanced techniques from algebraic geometry and modular forms.

But in the meantime, many mathematicians have made partial progress on the problem.
In particular, Sophie Germain's theorem states that \<^term>‹p› is a prime
such that \<^term>‹2 * p + 1› is also a prime, then there are no integer
solutions to the equation \<^term>‹x ^ p + y ^ p = z ^ p› such that \<^term>‹p›
divides neither \<^term>‹x›, \<^term>‹y› nor \<^term>‹z›.

This result is not only included in the extended list of Freek's ``Top 100 theorems''
⁋‹🌐‹http://www.cs.ru.nl/~freek/100/››,
but is also very familiar to students taking the French
``agrégation'' mathematics competitive examination.
Hoping that this submission might also be useful to them,
we developed separately the classical version of the theorem
as presented in \<^cite>‹Francinou_Gianella_Nicolas_2014›
and a generalization that one can find for example in \<^cite>‹kiefer2012theoreme›.›

text ‹
\begin{figure}[h]
\label{sessionGraph}
\centering
\includegraphics[scale=0.5]{session_graph} 
\caption{Dependency graph of the session \<^session>‹Sophie_Germain›}
\end{figure}
\newpage
›

text ‹
The session displayed in \ref{sessionGraph} is organized as follows:
  ▪ ▩‹FLT_Sufficient_Conditions› provides sufficient conditions for proving FLT,
  ▪ ▩‹SG_Premilinaries› establish some useful lemmas and introduces the concept
    of Sophie Germain prime,
  ▪ ▩‹SG_Theorem› proves Sophie Germain's theorem and
  ▪ ▩‹SG_Generalization› gives a generalization of it.
›



(*<*)
end

end
  (*>*)