×

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
Related Software: HOL Light; Isabelle/HOL; Coq; kepler98; Mizar; HOL; Isabelle; E Theorem Prover; VAMPIRE; Sledgehammer; TPTP; MaLARea; Tame Graphs; HOLyHammer; ML; MPTP 0.2; MaSh; ACL2; MaLeCoP; Metis_
Referenced in: 122 Publications
all top 5

Referenced by 159 Authors

26 Kaliszyk, Cezary
25 Urban, Josef
8 Hales, Thomas Callister
7 Nipkow, Tobias
6 Magron, Victor
6 Tahar, Sofiène
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 Jakubův, Jan
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 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 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 Chvalovský, Karel
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
1 Lightfoot, Olga
...and 59 more Authors

Referencing Publications by Year