1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
David M. Russinoff
david@russinoff.com
http://www.russinoff.com
This directory contains ACL2 proof scripts for some results of elementary
number theory. It includes the following ACL2 books:
euclid
Divisibility, primes, and two theorems of Euclid:
(1) The infinitude of the set of primes
(2) if p is a prime and p divides a * b, then p divides either a or b.
fermat
Fermat's Theorem: if p is a prime and p does not divide m, then
mod(m^(p-1),p) = 1.
euler
Quadratic residues and Euler's Criterion: if p is an odd prime and p does
not divide m, then
mod(m^((p-1)/2),p) = 1 if m is a quadratic residue mod p
p-1 if not.
A by-product of the proof is Wilson's Theorem: mod((p-1)!,p) = p-1.
As a consequence, we also prove the First Supplement to the Law of Quadratic
Reciprocity: -1 is a quadratic residue mod p iff mod(p,4) = 1.
gauss
Gauss's Lemma: Let p be an odd prime and let m be relatively prime to p.
Let mu be the number of elements of the sequence
(mod(m,p), mod(2*m,p), ..., mod(((p-1)/2)*m,p))
that exceed (p-1)/2. Then m is a quadratic residue mod p iff mu is even.
As a corollary, we also prove the Second Supplement to the Law of Quadratic
Reciprocity: 2 is a quadratic residue mod p iff mod(p,8) is either 1 or -1.
eisenstein
A formalization of Eisenstein's proof of the law of quadratic reciprocity:
If p and q are distinct odd primes, then
(p is a quadratic residue mod q <=> q is a quadratic residue mod p)
<=>
((p-1)/2) * ((q-1)/2) is even.
mersenne
An application to the Mersenne prime problem by way of a theorem of Euler:
if p and 2*p+1 are both prime and mod(p,4) = 3, then 2^p-1 is divisible by
2*p+1")
pratt
Vaughn Pratt's method of prime certification applied to the prime 2^255 - 19.
|
