A FORMAL PROOF of the KEPLER CONJECTURE

Thomas Hales; Mark Adams; Gertrud Bauer; Tat Dat Dang; John Harrison; Le Truong Hoang; Cezary Kaliszyk; Victor Magron; Sean McLaughlin; Tat Thang Nguyen; Quang Truong Nguyen; Tobias Nipkow; Steven Obua; Joseph Pleso; Jason Rute; Alexey Solovyev; Thi Hoai An Ta; Nam Trung Tran; Thi Diep Trieu; Josef Urban; Ky Vu; Roland Zumkeller

doi:10.1017/fmp.2017.1

A FORMAL PROOF of the KEPLER CONJECTURE

Thomas Hales
, Mark Adams
, Gertrud Bauer
, Tat Dat Dang
, John Harrison
, Le Truong Hoang
, Cezary Kaliszyk
, Victor Magron
, Sean McLaughlin
, Tat Thang Nguyen
, Quang Truong Nguyen
, Tobias Nipkow
, Steven Obua
, Joseph Pleso
, Jason Rute
, Alexey Solovyev
, Thi Hoai An Ta
, Nam Trung Tran
, Thi Diep Trieu
, Josef Urban

Ky Vu, Roland Zumkeller

Informatics 7 - Chair of Theoretical Computer Science

University of Pittsburgh
Proof Technologies Ltd
Radboud University Nijmegen
ESG Elektroniksystem- und Logistik-GmbH
CanberraWeb
Intel Corporation
VAST
University of Innsbruck
UJF-Grenoble 1, CNRS VERIMAG UMR 5104
Amazon.com, Inc.
University of Edinburgh
Philips Electronics North America Corporation
The Pennsylvania State University
University of Utah
AXA China Region Insurance Company Limited
Czech Technical University in Prague
Chinese University of Hong Kong

Research output: Contribution to journal › Article › peer-review

305 Scopus citations

Abstract

This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

Original language	English
Article number	e2
Journal	Forum of Mathematics, Pi
Volume	5
DOIs	https://doi.org/10.1017/fmp.2017.1
State	Published - 2017

Access to Document

10.1017/fmp.2017.1

Cite this

Hales, T., Adams, M., Bauer, G., Dang, T. D., Harrison, J., Hoang, L. T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T. T., Nguyen, Q. T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T. H. A., Tran, N. T., Trieu, T. D., ... Zumkeller, R. (2017). A FORMAL PROOF of the KEPLER CONJECTURE. Forum of Mathematics, Pi, 5, Article e2. https://doi.org/10.1017/fmp.2017.1

@article{3fdf2c9143a54629bba02e34f24c7698,

title = "A FORMAL PROOF of the KEPLER CONJECTURE",

abstract = "This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.",

author = "Thomas Hales and Mark Adams and Gertrud Bauer and Dang, \{Tat Dat\} and John Harrison and Hoang, \{Le Truong\} and Cezary Kaliszyk and Victor Magron and Sean McLaughlin and Nguyen, \{Tat Thang\} and Nguyen, \{Quang Truong\} and Tobias Nipkow and Steven Obua and Joseph Pleso and Jason Rute and Alexey Solovyev and Ta, \{Thi Hoai An\} and Tran, \{Nam Trung\} and Trieu, \{Thi Diep\} and Josef Urban and Ky Vu and Roland Zumkeller",

note = "Publisher Copyright: {\textcopyright} 2017 The Author(s).",

year = "2017",

doi = "10.1017/fmp.2017.1",

language = "English",

volume = "5",

journal = "Forum of Mathematics, Pi",

issn = "2050-5086",

publisher = "Cambridge University Press",

}

TY - JOUR

T1 - A FORMAL PROOF of the KEPLER CONJECTURE

AU - Hales, Thomas

AU - Adams, Mark

AU - Bauer, Gertrud

AU - Dang, Tat Dat

AU - Harrison, John

AU - Hoang, Le Truong

AU - Kaliszyk, Cezary

AU - Magron, Victor

AU - McLaughlin, Sean

AU - Nguyen, Tat Thang

AU - Nguyen, Quang Truong

AU - Nipkow, Tobias

AU - Obua, Steven

AU - Pleso, Joseph

AU - Rute, Jason

AU - Solovyev, Alexey

AU - Ta, Thi Hoai An

AU - Tran, Nam Trung

AU - Trieu, Thi Diep

AU - Urban, Josef

AU - Vu, Ky

AU - Zumkeller, Roland

PY - 2017

Y1 - 2017

N2 - This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

AB - This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

UR - https://www.scopus.com/pages/publications/85038578618

U2 - 10.1017/fmp.2017.1

DO - 10.1017/fmp.2017.1

M3 - Article

AN - SCOPUS:85038578618

SN - 2050-5086

VL - 5

JO - Forum of Mathematics, Pi

JF - Forum of Mathematics, Pi

M1 - e2

ER -

A FORMAL PROOF of the KEPLER CONJECTURE

Abstract

Access to Document

Other files and links

Fingerprint

Cite this