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 Ttung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, Roland Zumkeller

Forum of Mathematics, Pi, 5, pp. 1-29, 2017.


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 |    doi:10.1017/fmp.2017.1  


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 An Ta and
Nam Trung Tran and Thi Diep Trieu and Josef Urban and Ky Vu and Roland Zumkeller},
year = {2017}
Nach oben scrollen