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 条

[1]

[Anonymous], J FRANC LANG APPL JF

[2]

[Anonymous], 2008, N. Am. Math. Soc

[3]

[Anonymous], 2006, MATH ALGORITHMS PROO

[4] THE 4 COLOR PROOF SUFFICES [J].

APPEL, K ;

HAKEN, W .

MATHEMATICAL INTELLIGENCER, 1986, 8 (01) :10-&

[5]

BAUER G, 2006, ARCH FORMAL PROOFS

[6]

Collins G. E., 1975, LECT NOTES COMPUT SC, V33, P134, DOI DOI 10.1007/3-540-07407-4_17

[7]

Denney E, 2000, LECT NOTES COMPUT SC, V1869, P108

[8] Sphere packings, V. Pentahedral prisms [J].

Ferguson, Samuel P. .

DISCRETE & COMPUTATIONAL GEOMETRY, 2006, 36 (01) :167-204

[9]

GARLOFF J, 1986, LECT NOTES COMPUT SC, V212, P37

[10]

Gonthier G., 2008, Notices Amer. Math. Soc., V55, P1382

← 1 2 3 4 5 →