author  wenzelm 
Wed, 17 May 2006 01:23:44 +0200  
changeset 19672  9be07d531694 
parent 17159  d5060118122e 
permissions  rwrr 
11060  1 

2 
\documentclass[11pt,a4paper]{article} 

11855  3 
\usepackage{graphicx} 
11060  4 
\usepackage{isabelle,isabellesym,pdfsetup} 
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 BoyerMoore 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:321, 
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} 