src/HOL/Old_Number_Theory/document/root.tex
author wenzelm
Sat Oct 10 16:26:23 2015 +0200 (2015-10-10)
changeset 61382 efac889fccbc
parent 58625 c78b2223f001
permissions -rw-r--r--
isabelle update_cartouches;
wenzelm@11060
     1
\documentclass[11pt,a4paper]{article}
wenzelm@11855
     2
\usepackage{graphicx}
wenzelm@11060
     3
\usepackage{isabelle,isabellesym,pdfsetup}
wenzelm@40945
     4
\usepackage{textcomp}
wenzelm@11060
     5
wenzelm@11060
     6
\urlstyle{rm}
wenzelm@11060
     7
\isabellestyle{it}
wenzelm@11060
     8
wenzelm@11060
     9
\begin{document}
wenzelm@11060
    10
wenzelm@11060
    11
\title{Some results of number theory}
paulson@13871
    12
\author{Jeremy Avigad\\
paulson@13871
    13
    David Gray\\
paulson@13871
    14
    Adam Kramer\\
paulson@13871
    15
    Thomas M Rasmussen}
paulson@13871
    16
wenzelm@11060
    17
\maketitle
wenzelm@11060
    18
paulson@13871
    19
\begin{abstract}
wenzelm@19672
    20
This is a collection of formalized proofs of many results of number theory.
paulson@13871
    21
The proofs of the Chinese Remainder Theorem and Wilson's Theorem are due to
paulson@13871
    22
Rasmussen.  The proof of Gauss's law of quadratic reciprocity is due to
paulson@13871
    23
Avigad, Gray and Kramer.  Proofs can be found in most introductory number
paulson@13871
    24
theory textbooks; Goldman's \emph{The Queen of Mathematics: a Historically
paulson@13871
    25
Motivated Guide to Number Theory} provides some historical context.
paulson@13871
    26
paulson@13871
    27
Avigad, Gray and Kramer have also provided library theories dealing with
paulson@13871
    28
finite sets and finite sums, divisibility and congruences, parity and
paulson@13871
    29
residues.  The authors are engaged in redesigning and polishing these theories
paulson@13871
    30
for more serious use.  For the latest information in this respect, please see
paulson@13871
    31
the web page \url{http://www.andrew.cmu.edu/~avigad/isabelle}.  Other theories
paulson@13871
    32
contain proofs of Euler's criteria, Gauss' lemma, and the law of quadratic
paulson@13871
    33
reciprocity.  The formalization follows Eisenstein's proof, which is the one
paulson@13871
    34
most commonly found in introductory textbooks; in particular, it follows the
paulson@13871
    35
presentation in Niven and Zuckerman, \emph{The Theory of Numbers}.
paulson@13871
    36
paulson@13871
    37
To avoid having to count roots of polynomials, however, we relied on a trick
paulson@13871
    38
previously used by David Russinoff in formalizing quadratic reciprocity for
paulson@13871
    39
the Boyer-Moore theorem prover; see Russinoff, David, ``A mechanical proof
paulson@13871
    40
of quadratic reciprocity,'' \emph{Journal of Automated Reasoning} 8:3-21,
paulson@13871
    41
1992.  We are grateful to Larry Paulson for calling our attention to this
paulson@13871
    42
reference.
paulson@13871
    43
\end{abstract}
paulson@13871
    44
wenzelm@11060
    45
\tableofcontents
wenzelm@11855
    46
wenzelm@11855
    47
\begin{center}
wenzelm@17159
    48
  \includegraphics[scale=0.5]{session_graph}  
wenzelm@11855
    49
\end{center}
wenzelm@11855
    50
wenzelm@11060
    51
\newpage
wenzelm@11060
    52
wenzelm@11060
    53
\parindent 0pt\parskip 0.5ex
wenzelm@11060
    54
\input{session}
wenzelm@11060
    55
wenzelm@58625
    56
\bibliographystyle{abbrv}
wenzelm@58625
    57
\bibliography{root}
wenzelm@58625
    58
wenzelm@11060
    59
\end{document}