A formal proof of the Kepler conjecture
- Hales, T
- Adams, M
- Bauer, G
- Dang, DT
- Harrison, J
- Hoang, TL
- Kaliszyk, C
- Magron, V
- McLaughlin, S
- Nguyen, TT
- Nguyen, TQ
- Nipkow, T
- Obua, S
- Pleso, J
- Rute, J
- Solovyev, A
- Ta, AHT
- Tran, TN
- Trieu, DT
- Urban, J
- Vu, KK
- Zumkeller, R
Publication date
January 2015
DOIAbstract
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
Add to ORKG