Communicating formal proofs: the case of Flyspeck

DOI10.1007/978-3-642-39634-2_32MaRDI QIDQ5327363zbMATH OpenOpenAlexWikidataFDO

Authors Carst Tankink, Cezary Kaliszyk, Josef Urban, Herman Geuvers

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

Recommendations

• Formal mathematics on display: a wiki for Flyspeck
• Flyspecking Flyspeck
• An approach to literate and structured formal developments
• Cooperative Repositories for Formal Proofs
• scientific article; zbMATH DE number 1024410

Cited in

(9)

• An approach to literate and structured formal developments
• Flyspeck
• Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry
• Formal mathematics on display: a wiki for Flyspeck
• Point-and-write -- documenting formal mathematics by reference
• ProofScript: proof scripting for the masses
• A Wiki for Mizar: motivation, considerations, and initial prototype
• Proof auditing formalised mathematics
• Towards Knowledge Management for HOL Light

Describes a project that uses

Uses Software

• Proviola
• Coq
• HOL Light

This page was built for publication: Communicating formal proofs: the case of Flyspeck

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327363)