## A Mechanical Proof of Quadratic Reciprocity

### David M. Russinoff

#### Abstract

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)