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 ZUMKELLERForum of Mathematics, Pi, 5, pp. 1-29, 2017.
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 AN TA and
NAM TRUNG TRAN and
THI DIEP TRIEU and
JOSEF URBAN and
KY VU and
ROLAND ZUMKELLER},
year={2017}
}