A formal proof of the Kepler conjecture

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

A formal proof of the Kepler conjecture

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

School of Informatics

Research output: Working paper

Abstract / Description of output

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
Number of pages	21
Publication status	Published - 9 Jan 2015

Keywords / Materials (for Non-textual outputs)

math.MG
cs.LO

Access to Document

pdf

http://arxiv.org/abs/1501.02155

Cite this

@techreport{0c7b4a129a7f4d718fae8c1961df368d,

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.",

keywords = "math.MG, cs.LO",

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

year = "2015",

month = jan,

day = "9",

language = "English",

type = "WorkingPaper",

}

TY - UNPB

T1 - A formal proof of the Kepler conjecture

AU - Hales, Thomas

AU - Adams, Mark

AU - Bauer, Gertrud

AU - Tat Dang, Dat

AU - Harrison, John

AU - Le Hoang, Truong

AU - Kaliszyk, Cezary

AU - Magron, Victor

AU - McLaughlin, Sean

AU - Tat Nguyen, Thang

AU - Quang Nguyen, Truong

AU - Nipkow, Tobias

AU - Obua, Steven

AU - Pleso, Joseph

AU - Rute, Jason

AU - Solovyev, Alexey

AU - Hoai Thi Ta, An

AU - Nam Tran, Trung

AU - Thi Trieu, Diep

AU - Urban, Josef

AU - Khac Vu, Ky

AU - Zumkeller, Roland

PY - 2015/1/9

Y1 - 2015/1/9

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.

KW - math.MG

KW - cs.LO

M3 - Working paper

BT - A formal proof of the Kepler conjecture

ER -

A formal proof of the Kepler conjecture

Abstract / Description of output

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this