Proof Auditing Formalised Mathematics
Adams, Mark Miles
Journal of Formalized Reasoning, Volume 9 (2016), / Harvested from Journal of Formalized Reasoning

The first three formalisations of major mathematical proofs have heralded a new age 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 in checking, or even much concern that such checks have not been performed. In this paper, we motivate why we should be concerned about correctness, and argue the need for proof auditing, to rigorously and independently check a formalisation. We discuss the issues involved in performing an audit, and propose an effective and efficient auditing process. Throughout we use the Flyspeck Project, that formalises the Kepler Conjecture proof, to illustrate our point.

Published online : 2016-01-01
     title = {Proof Auditing Formalised Mathematics},
     journal = {Journal of Formalized Reasoning},
     volume = {9},
     year = {2016},
     doi = {10.6092/issn.1972-5787/4576},
     language = {EN},
     url = {}
Adams, Mark Miles. Proof Auditing Formalised Mathematics. Journal of Formalized Reasoning, Volume 9 (2016) . doi : 10.6092/issn.1972-5787/4576.