Flyspeck
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.
Keywords for this software
References in zbMATH (referenced in 107 articles , 2 standard articles )
Showing results 1 to 20 of 107.
Sorted by year (- Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
- Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
- Johansson, Moa: Lemma discovery for induction. A survey (2019)
- Rashid, Adnan; Hasan, Osman: Formal analysis of continuous-time systems using Fourier transform (2019)
- Stojanović-Ðurđević, Sana: From informal to formal proofs in Euclidean geometry (2019)
- Straßburger, Lutz: The problem of proof identity, and why computer scientists should care about Hilbert’s 24th problem (2019)
- Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
- Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Hamami, Yacin: Mathematical inference and logical inference (2018)
- Magron, Victor: Interval enclosures of upper bounds of roundoff errors using semidefinite programming (2018)
- Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
- Aransay, Jesús; Divasón, Jose: A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (2017)
- Beeson, Michael; Wos, Larry: Finding proofs in Tarskian geometry (2017)
- Cheung, Kevin K. H.; Gleixner, Ambros; Steffy, Daniel E.: Verifying integer programming results (2017)
- Eckl, Thomas: Kähler packings and Seshadri constants on projective complex surfaces (2017)
- Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef: TacticToe: learning to reason with HOL4 tactics (2017)
- Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang, Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland: A formal proof of the Kepler conjecture (2017)
- Jakubův, Jan; Urban, Josef: ENIGMA: efficient learning-based inference guiding machine (2017)
- Musin, O. R.: Towards a proof of the 24-cell conjecture (2017)