77
IRUS TotalDownloads
Altmetric
A formal proof of the Kepler conjecture
| File | Description | Size | Format | |
|---|---|---|---|---|
 1501.02155v1.pdf | Working paper | 174.87 kB | Adobe PDF | View/Open |
| Title: | A formal proof of the Kepler conjecture |
| Authors: | 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 |
| Item Type: | Report |
| 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. |
| Issue Date: | 18-Aug-2015 9-Jan-2015 |
| URI: | http://hdl.handle.net/10044/1/25725 |
| DOI: | https://doi.org/10.25561/25725 |
| Copyright Statement: | © 2015 The Authors |
| Notes: | 21 pages |
| Appears in Collections: | Electrical and Electronic Engineering Faculty of Engineering |