Trustworthy Storage and Exchange of Theorems

A large effort is usually required to have a theorem prover establish a complex theorem. Having invested this effort, how can we store the result for later use, or communicate it to others while preserving our trust in its validity? This paper discusses the use of digital signatures to store and exchange theorems in a secure way. 1 Introduction Suppose you have gone to the trouble of proving a theorem using a mechanical theorem prover. If your work is to have any enduring value, you have to be able to save your result for later use and communicate it to others. A theorem prover should allow its users to create and modify theorems only in a sound way. However, once outside the theorem prover --- for example while saved on disk or being transmitted elsewhere --- nothing protects a result from being modified in other ways. At present, this problem is not really addressed in the design of mechanical theorem provers. Some theorem provers --- like GETFOL [9] and Isabelle [16] --- can not sa..