Proof Auditing Formalised Mathematics
DOI:
https://doi.org/10.6092/issn.1972-5787/4576Keywords:
formal proof, Flyspeck, HOL Light, HOL Zero, Common HOL, proof auditingAbstract
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.References
Y Bertot & P Casteran. Interactive Theorem Proving and Program Develop-
ment: Coq’Art: The Calculus of Inductive Constructions. Springer, 2004.
R. Boyer et al. The QED Manifesto. In Proceedings of the 12th International
Conference on Automated Deduction, Volume 814 of Lecture Notes in Computer Science, Springer, 1994.
G. Gonthier. The Four Colour Theorem: Engineering of a Formal Proof. In
Proceedings of the 8th Asian Symposium of Computer Mathematics, Springer,
G. Gonthier et al. A Machine-Checked Proof of the Odd Order Theorem. In Proceedings of the 4th International Conference on Interactive Theorem Proving, Springer, 2013.
T. Hales & S. Ferguson. A Formulation of the Kepler Conjecture. Volume 36(1) of Discrete and Computational Geometry, 2006.
T. Hales. Introduction to the Flyspeck Project. In Mathematics, Algorithms,
Proofs, Volume 05021 of Dagstuhl Seminar Proceedings Internationales
Begegnungs- und Forschungszentrum f ̈r Informatik, 2005.
T. Hales et al. A Revision of the Proof of the Kepler Conjecture. Vomume 44(1) of Discrete and Computational Geometry, Springer, 2010.
T. Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Volume 400 of London Mathematical Society Lecture Note Series, Cambridge University Press, 2012.
T. Hales et al. A Formal Proof of the Kepler Conjecture. Submitted for publi-
cation in 2014.
J. Harrison. HOL Light: An Overview. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Springer, 2009.
J. Hurd. The Open Theory Standard Theory Library. In Third International
Symposium on NASA Formal Methods, Volume 6617 of Lecture Notes in Computer Science, Springer, 2011.
M. Gordon. An Introduction to the HOL System. In Proceedings of the 1991
International Workshop on the HOL Theorem Proving System and its Applications, IEEE Computer Society Press, 1992.
M. Gordon, R. Milner & C. Wadsworth. Edinburgh LCF: A Mechanised Logic
of Computation., Volume 78 of Lecture Notes in Computer Science, Springer,
C. Kaliszyk & A. Krauss. Scalable LCF-style Proof Translation. In Proceedings of the 4th International Conference on Interactive Theorem Proving, Springer, 2013.
C. Keller & B. Werner Importing HOL Light into Coq. In Proceedings of the
First International Conference on Interactive Theorem Proving, Springer, 2010.
R. Kumar et al. CakeML: A Verified Implementation of ML. 2014.
R. Kumar et al. HOL with Definitions: Semantics, Soundness, and a Verified
Implementation. 2014.
D. MacKenzie. Mechanizing Proof: Computing, Risk, and Trust. MIT Press,
T. Nipkow, L. Paulson & M. Wenzel. Isabelle/HOL: A Proof Assistant for
Higher-Order Logic. Volume 2283 of Lecture Notes in Computer Science,
Springer, 2002.
S. Obua & S. Skalberg. Importing HOL into Isabelle/HOL. In Proceedings of
Third International Joint Conference on Automated Reasoning, Springer, 2006.
R. Pollack. How to Believe a Machine-Checked Proof. In Twenty Five Years of Constructive Type Theory, Oxford University Press, 1998.
A. Trybulec & H. Blair. Computer Assisted Reasoning with MIZAR. In Pro-
ceedings of the 9th International Joint Conference on Artificial Intelligence,
Morgan Kaufmann, 1985.
F. Wiedijk. Comparing Mathematical Provers. In Second International Con-
ference on Mathematical Knowledge Management, Springer, 2003.
F. Wiedijk (Ed.). The Seventeen Provers of the World. In Volume 3600 of
Lecture Notes in Computer Science, Springer, 2006.
F. Wiedijk. Pollack-Inconsistency. In Volume 285 of Electronic Notes in Theoretical Computer Science, Elsevier Science, 2012.
W. Wong Validation of HOL Proofs by Proof Checking.. Formal Mehods in
System Design 14, Kluwer Academic Publishers, 1999.
Flyspeck homepage: http://code.google.com/p/flyspeck/
Odd Order formalisation homepage:
http://gforge.inria.fr/frs/?group id=401
Common HOL homepage: www.proof-technologies.com/commonhol/
HOL Zero homepage: www.proof-technologies.com/holzero/
Proof Technologies Flyspeck homepage:
www.proof-technologies.com/flyspeck/
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2016 Mark Miles Adams
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
