Communicating Formal Proofs: The Case of Flyspeck

Abstract. We introduce a platform for presenting and cross-linking for-mal and informal proof developments together. The platform supports writing natural language ‘narratives ’ that include islands of formal text. The formal text contains hyperlinks and gives on-demand state infor-mation for each proof step. We argue that such a system significantly lowers the threshold for understanding formal development and facili-tates collaboration on informal and formal parts of large developments. As an example, we show the Flyspeck formal development (in HOL Light) and the Flyspeck informal mathematical text as a narrative linked to the formal development. To make this possible, we use the Agora system, a MathWiki platform developed at Nijmegen which has so far mainly been used with the Coq theorem prover: we show that the system itself is generic and easily adapted to the HOL Light case.