A formal proof of the Kepler conjecture

File Description SizeFormat 
1501.02155v1.pdfWorking paper174.87 kBAdobe PDFView/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
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
URI: http://hdl.handle.net/10044/1/25725
Copyright Statement: © 2015 The Authors
Notes: 21 pages
Appears in Collections:Faculty of Engineering
Electrical and Electronic Engineering

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commonsx