\documentclass[11pt,a4paper,twoside]{article}
\usepackage[T1]{fontenc}

\addtolength{\textwidth}{1cm}
\addtolength{\textheight}{1cm}
\addtolength{\hoffset}{-.5cm}
\addtolength{\voffset}{-.5cm}
\addtolength{\oddsidemargin}{24pt}
\addtolength{\evensidemargin}{-24pt}
\usepackage{isabelle,isabellesym}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{fancyhdr}

\pagestyle{fancyplain}

\renewcommand{\headrulewidth}{1.6pt}
\renewcommand{\sectionmark}[1]{\markboth{\thesection\ #1}{\thesection\ #1}}
\renewcommand{\subsectionmark}[1]{\markright{\thesubsection\ #1}}

\lhead[\thepage]                                            
      {\fancyplain{}{\rightmark}}

\chead{}

\rhead[\fancyplain{}{\leftmark}]
      {\thepage}
                                      
\cfoot{}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Sums of two and four squares}
\author{Roelof Oosterhuis\\University of Groningen}
\maketitle

\begin{abstract}
This document gives the formal proofs of the following results about the sums of two and four squares:
\begin{enumerate}
\item Any prime number $p \equiv 1 \bmod 4$ can be written as the sum of two squares.
%\item No prime number $p \equiv 3 \bmod 4$ can be written as the sum of two squares.
%\item For any prime number $p \equiv 3 \bmod 4$ we have: $n$ can be written as the sum of two squares if and only if $np^2$ can be written as the sum of two squares.
\item (Lagrange) Any natural number can be written as the sum of four squares.
\end{enumerate}
%Note that 1--3 completely determine the numbers that can be written as the sum of two squares.\\
The proofs are largely based on chapters II and III of the book by
Weil~\cite{Weil}.

The results %1--3 already have been formalised in the proof assistant `Coq'\footnote{See \href{http://coq.inria.fr/contribs/SumOfTwoSquare.html}{http://coq.inria.fr/contribs/SumOfTwoSquare.html}} and the results 1 and 4 
have been formalised before in the proof assistant HOL Light~\cite{HOLLight}. A more complete study of the sum of two squares, including the first result, has been formalised in Coq~\cite{Thery}.
The results can also be found as numbers 20 and 19 on the list of `top 100 mathematical theorems' \cite{Wiedijk100}.

This research is part of an M.Sc.~thesis under supervision of Jaap Top
and Wim H.~Hesselink (RU Groningen). For more information see
\cite{Oosterhuis-MSc}.
\end{abstract}
\thispagestyle{empty}
\clearpage

\markboth{Contents}{Contents}
\tableofcontents
\markboth{Contents}{Contents}

%\vspace{1cm}
%\begin{figure}[hb]
%\centering
%\includegraphics[scale=0.5]{sumsq.pdf}
%\caption{The depence on existing files in the Isabelle library.}
%\end{figure}
%\clearpage

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{alpha}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
