summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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}

6 \urlstyle{rm}

7 \isabellestyle{it}

9 \begin{document}

11 \title{Some results of number theory}

12 \author{Jeremy Avigad\\

13 David Gray\\

14 Adam Kramer\\

15 Thomas M Rasmussen}

17 \maketitle

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.

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

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}

45 \tableofcontents

47 \begin{center}

48 \includegraphics[scale=0.5]{session_graph}

49 \end{center}

51 \newpage

53 \parindent 0pt\parskip 0.5ex

54 \input{session}

56 \bibliographystyle{abbrv}

57 \bibliography{root}

59 \end{document}