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