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}