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.