Communicating and trusting proofs: The case for foundational proof certificates

To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science in Nancy, France, 19-26 July 2011.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 is checked for its syntactic correctness, one can then trust that the theorem is, in fact, true. In this paper, we argue that structural proof theory and computer automation have matured to such a level that they can be used to provide a flexible and universal approach to proof-as-certificate. In contrast, the notion of proof-as-message is still evolving and deals with structures, such as diagrams and natural language texts, that are not yet well formalized