Abstract: The first three formalisations of major mathematical proofs, all in the last decade, have heralded a new era in formalised mathematics, establishing that informal proofs at the limits of what can be understood by humans can be checked by machine. However, formalisation itself can be subject to error, and yet there is currently no accepted process of checking, or even much concern that such checks have not been performed. In this paper, we explain why formalisation proofs should be checked, and propose rigorous and independent proof auditing. We discuss the issues involved in performing an audit, and propose an effective auditing process. We use the Flyspeck project, one of the major formalisations, to illustrate our point, and subject it to a partial audit.
Download PDF: qed_paper.pdf
Reference: M.Adams. Proof Auditing Formalised Mathematics. In Volume 9(1) of Journal of Formalized Reasoning, pages 3-32. 2016.