src/HOL/Old_Number_Theory/document/root.tex
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 58625 c78b2223f001 permissions -rw-r--r--
tuned proofs;
     1 \documentclass[11pt,a4paper]{article}

     2 \usepackage{graphicx}

     3 \usepackage{isabelle,isabellesym,pdfsetup}

     4 \usepackage{textcomp}

     5

     6 \urlstyle{rm}

     7 \isabellestyle{it}

     8

     9 \begin{document}

    10

    11 \title{Some results of number theory}

    12 \author{Jeremy Avigad\\

    13     David Gray\\

    14     Adam Kramer\\

    15     Thomas M Rasmussen}

    16

    17 \maketitle

    18

    19 \begin{abstract}

    20 This is a collection of formalized proofs of many results of number theory.

    21 The proofs of the Chinese Remainder Theorem and Wilson's Theorem are due to

    22 Rasmussen.  The proof of Gauss's law of quadratic reciprocity is due to

    23 Avigad, Gray and Kramer.  Proofs can be found in most introductory number

    24 theory textbooks; Goldman's \emph{The Queen of Mathematics: a Historically

    25 Motivated Guide to Number Theory} provides some historical context.

    26

    27 Avigad, Gray and Kramer have also provided library theories dealing with

    28 finite sets and finite sums, divisibility and congruences, parity and

    29 residues.  The authors are engaged in redesigning and polishing these theories

    30 for more serious use.  For the latest information in this respect, please see

    31 the web page \url{http://www.andrew.cmu.edu/~avigad/isabelle}.  Other theories

    32 contain proofs of Euler's criteria, Gauss' lemma, and the law of quadratic

    33 reciprocity.  The formalization follows Eisenstein's proof, which is the one

    34 most commonly found in introductory textbooks; in particular, it follows the

    35 presentation in Niven and Zuckerman, \emph{The Theory of Numbers}.

    36

    37 To avoid having to count roots of polynomials, however, we relied on a trick

    38 previously used by David Russinoff in formalizing quadratic reciprocity for

    39 the Boyer-Moore theorem prover; see Russinoff, David, A mechanical proof

    40 of quadratic reciprocity,'' \emph{Journal of Automated Reasoning} 8:3-21,

    41 1992.  We are grateful to Larry Paulson for calling our attention to this

    42 reference.

    43 \end{abstract}

    44

    45 \tableofcontents

    46

    47 \begin{center}

    48   \includegraphics[scale=0.5]{session_graph}

    49 \end{center}

    50

    51 \newpage

    52

    53 \parindent 0pt\parskip 0.5ex

    54 \input{session}

    55

    56 \bibliographystyle{abbrv}

    57 \bibliography{root}

    58

    59 \end{document}