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
Forum of Mathematics, Pi, 5, pp. 1-29, 2017.

pdf   doi:10.1017/fmp.2017.1

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.

BibTex

@article{thetal-pi17,
title={A Formal Proof of the {K}epler conjecture},
volume={5},
doi={10.1017/fmp.2017.1},
journal={Forum of Mathematics, Pi},
publisher={Cambridge University Press},
author={
Thomas Hales and
Mark Adams and
Gertrud Bauer and
Tat Dat Dang and
John Harrison and
Le Truong Hoang and
Cezary Kaliszyk and
Victor Magron and
Sean McLaughlin and
Tat Thang Nguyen and
Quang Truong Nguyen and
Tobias Nipkow and
Steven Obua and
Joseph Pleso and
Jason Rute and
Alexey Solovyev and
Thi Hoai Aa Ta and
Nam Trung Tran and
Thi Diep Trieu and
Josef Urban and
Ky Vu and
Roland Zumkeller},
year={2017}
}