@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",
}