A FORMAL PROOF OF THE KEPLER CONJECTURE
type: Item
instance of: scholarly article
title: A FORMAL PROOF OF THE KEPLER CONJECTURE
zbMATH Open document ID: 1379.52018
published in: Forum of Mathematics, Pi
publication date: 2017-07-20T00:00:00Z
full work available at URL: https://arxiv.org/abs/1501.02155
Mathematics Subject Classification ID: 52C17
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6750549
zbMATH Keywords: ball packing
zbMATH Keywords: Kepler conjecture
zbMATH Keywords: formal proof
zbMATH Keywords: Flyspeck project
zbMATH Keywords: HOL Light proof assistant
zbMATH Keywords: Isabelle proof assistant
describes a project that uses: GLPK
describes a project that uses: LCF
describes a project that uses: Archive Formal Proofs
describes a project that uses: GNU parallel
describes a project that uses: Tame Graphs
describes a project that uses: HOL Light
describes a project that uses: Isabelle/HOL
describes a project that uses: HOL
describes a project that uses: ML
describes a project that uses: Flyspeck
describes a project that uses: kepler98
describes a project that uses: seL4
describes a project that uses: HOL Zero
describes a project that uses: GitHub
MaRDI profile type: Publication
OpenAlex ID: W1825294361
Wikidata QID: Q56267705
arXiv ID: 1501.02155
cites work: Flyspecking Flyspeck
cites work: Flyspeck I: Tame Graphs
cites work: Q5824053
cites work: A Machine-Checked Proof of the Odd Order Theorem
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Q5287513
cites work: Code Generation via Higher-Order Rewrite Systems
cites work: Developments in Formal Proofs
cites work: A proof of the Kepler conjecture
cites work: Dense sphere packings. A blueprint for formal proofs
cites work: A formulation of the Kepler conjecture
cites work: A revision of the proof of the Kepler conjecture
cites work: Towards Self-verification of HOL Light
cites work: Without Loss of Generality
cites work: HOL Light: An Overview
cites work: Scalable LCF-Style Proof Translation
cites work: Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
cites work: Learning-assisted theorem proving with millions of lemmas
cites work: HOL with Definitions: Semantics, Soundness, and a Verified Implementation
cites work: Formal certification of a compiler back-end or
cites work: Study of the Kepler's conjecture: the problem of the closest packing
cites work: An Interpretation of Isabelle/HOL in HOL Light
cites work: Introduction to Interval Analysis
cites work: Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Theorem Proving in Higher Order Logics
cites work: Flyspeck II: The basic linear programs
cites work: Efficient Formal Verification of Bounds of Linear Programs
cites work: Formal Mathematics on Display: A Wiki for Flyspeck
DOI: 10.1017/FMP.2017.1
description: scientific article; zbMATH DE number 6750549