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

doi:https://doi.org/10.25561/25725

File(s)

1501.02155v1.pdf (174.87 KB)

Working paper

Author(s)

Hales, T

Adams, M

Bauer, G

Dang, DT

Harrison, J

more

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.

Date Issued

2015-08-18T09:05:46Z

2015-01-09

URI

http://hdl.handle.net/10044/1/25725

DOI

https://doi.org/10.25561/25725

Copyright Statement

License URL

http://www.rioxx.net/licenses/all-rights-reserved

Identifier

http://arxiv.org/abs/1501.02155v1

Notes

21 pages