Proof auditing formalised mathematics

DOI10.6092/ISSN.1972-5787/4576MaRDI QIDQ5195266zbMATH OpenOpenAlexFDO

Authors

Publication date 18 September 2019

Full work available at URL https://doaj.org/article/92814624a1c54850b64dbdf3c0bbaee0

zbMATH Keywords

formal proofFlyspeckHOL lightcommon HOLHOL zeroproof-auditing

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Flyspecking Flyspeck
• Formal proof
• Types for Proofs and Programs
• scientific article; zbMATH DE number 1302064
• Communicating formal proofs: the case of Flyspeck

Cites work

• scientific article; zbMATH DE number 2127501 (Why is no real title available?)
• scientific article; zbMATH DE number 3907807 (Why is no real title available?)
• scientific article; zbMATH DE number 1302064 (Why is no real title available?)
• scientific article; zbMATH DE number 1321106 (Why is no real title available?)
• scientific article; zbMATH DE number 1951639 (Why is no real title available?)
• A formulation of the Kepler conjecture
• A machine-checked proof of the odd order theorem
• A revision of the proof of the Kepler conjecture
• Analysis 2.
• CakeML
• Dense sphere packings. A blueprint for formal proofs
• Edinburgh LCF. A mechanized logic of computation
• HOL Light: An Overview
• HOL with definitions: semantics, soundness, and a verified implementation
• Importing HOL Light into Coq
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Pollack-inconsistency
• Scalable LCF-style proof translation
• The Four Colour Theorem: Engineering of a Formal Proof
• The seventeen provers of the world. Foreword by Dana S. Scott..
• Theorem Proving in Higher Order Logics

Cited in

(3)

• scientific article; zbMATH DE number 1951637 (Why is no real title available?)
• Declarative Proof Translation (Short Paper)
• Semantics of Mizar as an Isabelle object logic

Describes a project that uses

Uses Software

• kepler98
• Flyspeck
• CakeML
• HOL Light
• HOL
• Mizar
• Coq

This page was built for publication: Proof auditing formalised mathematics

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