Proof Auditing Formalised Mathematics

DOI10.6092/issn.1972-5787/4576zbMath1451.68328OpenAlexW2258253484MaRDI QIDQ5195266

No author found.

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)

Related Items (2)

Declarative Proof Translation (Short Paper) ⋮ Semantics of Mizar as an Isabelle object logic

Uses Software

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

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• A formulation of the Kepler conjecture
• The seventeen provers of the world. Foreword by Dana S. Scott..
• A revision of the proof of the Kepler conjecture
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• HOL Light: An Overview
• The Four Colour Theorem: Engineering of a Formal Proof
• Pollack-inconsistency
• Scalable LCF-Style Proof Translation
• A Machine-Checked Proof of the Odd Order Theorem
• CakeML
• Theorem Proving in Higher Order Logics
• Importing HOL Light into Coq
• Analysis 2.
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof Auditing Formalised Mathematics