Checking number theory proofs in natural language

Proofs in natural language contain much information useful for automatic proof checking that is usually lost in translation to a formal language. We describe a system which checks English language proofs in elementary number theory that uses such information to guide the theorem prover. The input to the system is a number theory proof written in the L scAT$\sb{\rm E}$X formatting language. The proof connector follows the argument presented in the proof and asks a theorem prover to make the same deductions that the human reader of the proof is assumed to make. The result is a more formal equivalent of the original informal natural language proof. This system can thus be used to extend the power of theorem provers by allowing the user to specify not only what the steps of the proof are, but also to specify, in a natural way, how the steps combine to form the whole proof.