We describe the use of the Boyer-Moore theorem prover in mechanically generating a proof of the Law of Quadratic Reciprocity. The proof is a formalization of an argument due to Eisenstein, based on a lemma of Gauss. We present a complete account of the input to the theorem prover, consisting of recursive function definitions, conjectures, and hints for proving them. The proofs are derived from a library of lemmas that includes Fermat's and Wilson's Theorems.
Full paper: ps, pdf (appeared in Journal of Automated Reasoning, 8: 3-21, 1992)