Flyspecking Flyspeck
In the past 15 years, theorem provers have been successfully employed in the
formalisation of three significant mathematical results: the Four-Colour
Theorem, the Feit-Thompson Lemma and the Kepler Conjecture. By mechanising the
process of formal proof, their usage has greatly increased assurance that these
important-but-complex proofs are correct. However, lingering doubts remain
about the soundness of the theorem provers themselves.
In this talk we describe a capability for addressing such concerns. We
concentrate on the Flyspeck Project, Hales' effort to formalise his proof of the
Kepler Conjecture using the HOL Light system and which is nearing completion.
We first explain why a sceptic might doubt the formalisation. We go on to
explain how the formal proof can be ported to the highly-trustworthy HOL Zero
system and then independently audited, thus resolving any doubts.