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;
     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}