Communicating and trusting proofs: The case for foundational proof certificates
Dale Armin Miller · 2013
It is well recognized that proofs serve two different goals. On one hand, they can serve the didactic purpose of explaining why a theorem holds: that is, a proof has a message that is meant to describe the “why ” behind a theorem. On the other hand, proofs can serve as certificates of validity. In this case, once a certificate