Communicating Formal Proofs: The Case of Flyspeck

DOI10.1007/978-3-642-39634-2_32zbMath1317.68232OpenAlexW1573268168WikidataQ108482174 ScholiaQ108482174MaRDI QIDQ5327363

Carst Tankink, Herman Geuvers, Cezary Kaliszyk, Josef Urban

Publication date: 7 August 2013

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2066/117354

Mathematics Subject Classification ID

Related Items

Flyspeck ⋮ Towards Knowledge Management for HOL Light ⋮ Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Coq
• Proviola
• HOL Light