A Formal Proof of the Kepler Conjecture

Tom Hales and many others including John Harrison.

ArXiV 1501.02155, 2015.

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.

PDF

Bibtex entry:

@ARTICLE{hales-kepler,
        author          = "Thomas C. Hales and
                           Mark Adams and
                           Gertrud Bauer and
                           Dat Tat Dang and
                           John Harrison and
                           Truong Le Hoang and
                           Cezary Kaliszyk and
                           Victor Magron and
                           Sean McLaughlin and
                           Thang Tat Nguyen and
                           Truong Quang Nguyen and
                           Tobias Nipkow and
                           Steven Obua and
                           Joseph Pleso and
                           Jason Rute and
                           Alexey Solovyev and
                           An Hoai Thi Ta and
                           Trung Nam Tran and
                           Diep Thi Trieu and
                           Josef Urban and
                           Ky Khac Vu and
                           Roland Zumkeller",
        title           = "A formal proof of the Kepler conjecture",
        journal         = "arXiv"
        volume          = "1501.02155",
        year            = 2015}