Flyspeck swMATH ID: 10277 Software Authors: Hales, Thomas C.; Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman Description: Communicating formal proofs: the case of flyspeck. We introduce a platform for presenting and cross-linking formal 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 information at every proof step. We argue that such a system significantly lowers the threshold for understanding formal development and facilitates 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. Homepage: https://github.com/flyspeck/flyspeck Source Code: https://github.com/flyspeck/flyspeck Related Software: HOL Light; Isabelle/HOL; Coq; kepler98; Mizar; HOL; E Theorem Prover; Isabelle; VAMPIRE; Sledgehammer; TPTP; MaLARea; Tame Graphs; HOLyHammer; MaSh; ML; MPTP 0.2; MaLeCoP; ACL2; BliStr Cited in: 125 Publications Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2013 Dense sphere packings. A blueprint for formal proofs. Zbl 1263.52001Hales, Thomas C. 2012 all top 5 Cited by 162 Authors 27 Urban, Josef 26 Kaliszyk, Cezary 8 Hales, Thomas Callister 7 Nipkow, Tobias 6 Magron, Victor 6 Tahar, Sofiène 5 Jakubův, Jan 5 Paulson, Lawrence Charles 5 Siddique, Umair 5 Vyskočil, Jiří 4 Bezdek, Károly 4 Blanchette, Jasmin Christian 4 Gauthier, Thibault 4 Geuvers, Jan Herman 3 Allamigeon, Xavier 3 Färber, Michael 3 Gaubert, Stéphane 3 Hasan, Osman 3 McLaughlin, Sean 3 Obua, Steven 3 Rabe, Florian 3 Schulz, Stephan 3 Sutcliffe, Geoff 3 Werner, Benjamin 2 Adams, Mark 2 Aransay, Jesús 2 Avigad, Jeremy 2 Bauer, Gertrud 2 Benzmüller, Christoph Ewald 2 Chvalovský, Karel 2 Guan, Yong 2 Hamami, Yacin 2 Harland, James A. 2 Janičić, Predrag 2 Khan Afshar, Sanaz 2 Narboux, Julien 2 Noschinski, Lars 2 Rubio García, Julio Jesús 2 Shi, Zhiping 2 Solovyev, Alexey 2 Stojanović Đurđević, Sana 2 Suda, Martin 2 Tankink, Carst 2 Wenzel, Makarius 2 Zumkeller, Roland 1 Aehlig, Klaus 1 Amato, Daniela A. 1 Angryk, Rafal A. 1 Anstreicher, Kurt M. 1 Aravantinos, Vincent 1 Ballarin, Clemens 1 Beeson, Michael J. 1 Böhme, Sascha 1 Brown, Chad Edward 1 Brucker, Achim D. 1 Bulwahn, Lukas 1 Bundy, Alan 1 Calude, Cristian S. 1 Carette, Jacques 1 Cherlin, Gregory L. 1 Cheung, Kevin K. H. 1 Cramer, Marcos 1 Czajka, Łukasz 1 Dang, Tat Dat 1 Divasón, Jose 1 Doczkal, Christian 1 Domínguez, César 1 Dunchev, Cvetan 1 Farmer, William M. 1 Fleuriot, Jacques D. 1 Fleury, Mathias 1 Gleixner, Ambros M. 1 Gottliebsen, Hanne 1 Gransden, Thomas 1 Greenaway, David 1 Haftmann, Florian 1 Hardy, Ruth 1 Heras, Jónathan 1 Heule, Marijn J. H. 1 Hoàng Lê Trường 1 Hölzl, Johannes 1 Horozal, Fulya 1 Immler, Fabian 1 Johansson, Moa 1 Joswig, Michael 1 Kallus, Yoav 1 Kerber, Manfred 1 Klein, Gerwin 1 Koepke, Peter 1 Kohlhase, Michael 1 Komendantskaya, Ekaterina 1 Kühlwein, Daniel 1 Kullmann, Oliver 1 Kumar, Ramana 1 Kusner, Wöden 1 Lagarias, Jeffrey C. 1 Lange, Christoph 1 Lángi, Zsolt 1 Larvor, Brendan P. 1 Li, Ximeng ...and 62 more Authors all top 5 Cited in 33 Serials 17 Journal of Automated Reasoning 5 Journal of Symbolic Computation 5 Mathematics in Computer Science 4 Theoretical Computer Science 4 Formal Aspects of Computing 4 Annals of Mathematics and Artificial Intelligence 3 Journal of Formalized Reasoning 2 Discrete Mathematics 2 Synthese 2 Discrete & Computational Geometry 2 The Review of Symbolic Logic 1 Letters in Mathematical Physics 1 The Mathematical Intelligencer 1 ACM Transactions on Mathematical Software 1 Journal of Geometry 1 Journal of Mathematical Economics 1 Acta Mathematica Hungarica 1 Journal of the American Mathematical Society 1 AI Communications 1 Differential Geometry and its Applications 1 Bulletin of the American Mathematical Society. New Series 1 Mathematical Programming. Series A. Series B 1 The Bulletin of Symbolic Logic 1 Documenta Mathematica 1 Journal of Combinatorial Optimization 1 Journal of Mathematical Logic 1 Journal of Applied Mathematics 1 Sādhanā 1 London Mathematical Society Lecture Note Series 1 Proceedings of the Steklov Institute of Mathematics 1 Forum of Mathematics, Pi 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 26 Fields 100 Computer science (68-XX) 23 Mathematical logic and foundations (03-XX) 18 Convex and discrete geometry (52-XX) 11 Combinatorics (05-XX) 9 General and overarching topics; collections (00-XX) 9 Operations research, mathematical programming (90-XX) 6 Number theory (11-XX) 5 Optics, electromagnetic theory (78-XX) 4 Algebraic geometry (14-XX) 4 Geometry (51-XX) 3 History and biography (01-XX) 3 Linear and multilinear algebra; matrix theory (15-XX) 3 Numerical analysis (65-XX) 2 Ordinary differential equations (34-XX) 1 Category theory; homological algebra (18-XX) 1 Group theory and generalizations (20-XX) 1 Real functions (26-XX) 1 Functions of a complex variable (30-XX) 1 Approximations and expansions (41-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Algebraic topology (55-XX) 1 Manifolds and cell complexes (57-XX) 1 Statistics (62-XX) 1 Quantum theory (81-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 Systems theory; control (93-XX) Citations by Year