A mechanical proof of Quadratic Reciprocity

We describe the use of the Boyer-Moore theorem prover in mechanically generating a proof of the Law of Quadratic Reciprocity: for distinct odd primes p and q, the congruences x ² q (mod p) and x ² p (mod q) are either both solvable or both unsolvable, unless pq3 (mod 4). The proof is a formalization of an argument due to Eisenstein, based on a lemma of Gauss. The input to the theorem prover consists of nine function definitions, thirty conjectures, and various hints for proving them. The proofs are derived from a library of lemmas that includes Fermat's Theorem and the Gauss Lemma.