At the request of David Russinoff, updated books/projects/quadratic-r…

…eciprocity/ and added books/projects/shnf/.

books/projects/quadratic-reciprocity/LICENSE

@@ -0,0 +1,35 @@
+Quadratic Reciprocity Library
+Author: David M. Russinoff
+
+Note: The license below is based on the template at:
+http://opensource.org/licenses/BSD-3-Clause
+
+Copyright (C) 2015, Intel Corp.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+o Redistributions of source code must retain the above copyright
+  notice, this list of conditions and the following disclaimer.
+
+o Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+
+o Neither the name of Intel Corporation nor the names of
+  its contributors may be used to endorse or promote products derived
+  from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

books/projects/quadratic-reciprocity/README

@@ -0,0 +1,53 @@
+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.
+