Proof Checking the RSA (Rivest, Shamir, and Adleman) Public Key Encryption Algorithm.

Typical proofs in journal articles, textbooks, and day-to-day mathematical communication use informal notation and leave many of the steps to the readers imagination. Nevertheless, by transcribing the sentences of the proof into a formal notation, it is sometimes possible to use todays automatic theorem-provers to fill in the gaps between published steps and thus mechanically check some published, informal proofs. In this paper we illustrate this idea by mechanically checking the recently published proof of the invertibility of the public encryption algorithm. We will briefly explain the idea of public key encryption to motivate the theorem proved.