A Revision of the Proof of the Kepler Conjecture

被引：49
作者：
Hales, Thomas C. [1 ]
Harrison, John [2 ]
McLaughlin, Sean [3 ]
Nipkow, Tobias [4 ]
Obua, Steven [4 ]
Zumkeller, Roland [5 ]
机构：
[1] Univ Pittsburgh, Dept Math, Pittsburgh, PA 15260 USA
[2] Intel Corp, Hillsboro, OR 97124 USA
[3] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
[4] Tech Univ Munich, Dept Informat, Munich, Germany
[5] Ecole Polytech, F-75230 Paris, France
来源：
DISCRETE & COMPUTATIONAL GEOMETRY | 2010年 / 44卷 / 01期
基金：
美国国家科学基金会;
关键词：
Formal proof; Sphere packings; Linear programming; Interval analysis; Higher order logic; Hypermap; SPHERE PACKINGS; HOL;
D O I：
10.1007/s00454-009-9148-4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original proof, announced in 1998 and published in 2006, is long and complex. The process of revision and review did not end with the publication of the proof. This article summarizes the current status of a long-term initiative to reorganize the original proof into a more transparent form and to provide a greater level of certification of the correctness of the computer code and other details of the proof. A final part of this article lists errata in the original proof of the Kepler conjecture.
引用
收藏
页码：1 / 34
页数：34
相关论文
共 49 条
[11]  
Hales T. C., 2008, NOT AM MATH SOC, V55, P1370
[12]   Historical overview of the Kepler conjecture [J].
Hales, TC .
DISCRETE & COMPUTATIONAL GEOMETRY, 2006, 36 (01) :5-20
[13]   Sphere packings, VI. Tame graphs and linear programs [J].
Hales, TC .
DISCRETE & COMPUTATIONAL GEOMETRY, 2006, 36 (01) :205-265
[14]   Sphere packing, III. Extremal cases [J].
Hales, TC .
DISCRETE & COMPUTATIONAL GEOMETRY, 2006, 36 (01) :71-110
[15]   Sphere packing, IV. Detailed bounds [J].
Hales, TC .
DISCRETE & COMPUTATIONAL GEOMETRY, 2006, 36 (01) :111-166
[16]   A proof of the Kepler conjecture [J].
Hales, TC .
ANNALS OF MATHEMATICS, 2005, 162 (03) :1065-1185
[17]   Sphere packings .1. [J].
Hales, TC .
DISCRETE & COMPUTATIONAL GEOMETRY, 1997, 17 (01) :1-51
[18]  
HALES TC, 2007, FLYSPECK PROJECT
[19]  
HALES TC, 2007, LICS 07, P35
[20]  
HALES TC, 2009, J AM MATH S IN PRESS
12345