Journal of the American Mathematical Society

Author(s): Thomas C. Hales; Sean McLaughlin
Journal: J. Amer. Math. Soc.
MSC (2010): Primary 52C17
Posted: October 27, 2009
Supplement: Additional materials posted with this article.
Retrieve article in: PDF

Abstract: This article gives a summary of a proof of Fejes Tóth's dodecahedral conjecture: the volume of a Voronoi polyhedron in a three-dimensional packing of balls of unit radius is at least the volume of a regular dodecahedron of unit inradius.

1.: G. Alefeld and J. Herzeberger.
Introduction to Interval Computations.
Academic Press, 1983. MR 733988 (85d:65001)
2.: G. Bauer.
Formalizing Plane Graph Theory - Towards a Formalized Proof of the Kepler Conjecture.
Ph.D. thesis, Technische Universität München, 2006.
3.: Y. Bertot and P. Castéran.
Interactive theorem proving and program development: Coq'Art: the Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. Springer-Verlag, 2004. MR 2229784 (2007i:68001)
4.: K. Bezdek.
Isoperimetric inequalities and the dodecahedral conjecture.
In International Journal of Mathematics, volume 8/6, pages 759-780, 1997. MR 1470853 (98k:52043)
5.: K. Bezdek.
On a stronger form of Rogers's lemma and the minimum surface area of Voronoi cells in unit ball packings.
In Journal fur die Reine und Angewandte Mathematik, volume 518, pages 131-143, 2000. MR 1739407 (2001b:52033)
6.: R. H. Byrd, J. N. Ocedal, and R. A. Waltz.
KNITRO: An integrated package for nonlinear optimization.
In G. di Pillo and M. Roma, editors, Large-Scale Nonlinear Optimization, pages 35-59. Springer-Verlag, 2006. MR 2194566 (2006h:90001)
7.: G. E. Collins.
Quantifier elimination for real closed fields by cylindrical algebraic decomposition.
In H. Brakhage, editor, Automata Theory and Formal Languages, volume 33 of Lecture Notes in Computer Science, pages 134-183, Berlin, 1975. Springer-Verlag. MR 0403962 (53:7771)
8.: L. Fejes Tóth.
Uber die dichteste Kugellagerung.
In Mathematische Zeitschrift, volume 48, pages 676-684, 1943. MR 0009129 (5:106f)
9.: L. Fejes Tóth.
Regular Figures.
Pergamon Press, Oxford, London, New York, 1964. MR 0165423 (29:2705)
10.: L. Fejes Tóth.
Lagerungen in der Ebene auf der Kugel und im Raum.
Springer-Verlag, Berlin-New York, second edition, 1972. MR 0353117 (50:5603)
11.: G. Gonthier.
A computer-checked proof of the four colour theorem.
Unpublished manuscript, 2005.
12.: T. Hales and S. McLaughlin.
An appendix to the dodecahedral conjecture.
http://www.ams.org/jams.
13.: T. C. Hales.
The Flyspeck Fact Sheet, 2003 (revised 2007).
http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet.
14.: T. C. Hales.
The status of the Kepler conjecture.
In Mathematical Intelligencer, volume 16/3, pages 47-58, 1994. MR 1281754 (95g:52033)
15.: T. C. Hales.
Sphere packings I.
In Discrete and Computational Geometry, volume 17, pages 1-51, 1997. MR 1418278 (97k:52025)
16.: T. C. Hales.
Some algorithms arising in the proof of the Kepler conjecture.
In Discrete and Computational Geometry, volume 25, pages 489-507, 2003. MR 2038488 (2005b:52047)
17.: T. C. Hales.
The Flyspeck Project, 2007.
http://code.google.com/p/flyspeck.
18.: T. C. Hales and S. P. Ferguson.
The Kepler conjecture.
Discrete and Computational Geometry, 36(1):1-269, 2006. MR 2229658 (2007d:52022)
19.: T. C. Hales and S. McLaughlin.
A proof of the dodecahedral conjecture (1998 version).
http://arxiv.org/abs/math/9811079v1.
20.: T. C. Hales and S. McLaughlin.
A proof of the dodecahedral conjecture (2002 version).
http://arxiv.org/abs/math/9811079v2.
21.: E. Harshbarger.
Saturated packings and Voronoi cells, 1996.
http://www.ericharshbarger.org/voronoi.html.
22.: J. F. Hart et al.
Computer Approximations.
John Wiley & Sons, 1968.
23.: L. Hörmander.
The Analysis of Linear Partial Differential Operators II, volume 257 of Grundlehren der mathematischen Wissenschaften.
Springer-Verlag, 1983. MR 705278 (85g:35002b)
24.: W.-Y. Hsiang.
On the sphere packing problem and the proof of Kepler's conjecture.
In International Journal of Mathematics, volume 4/5, pages 739-831, 1993. MR 1245351 (95g:52032)
25.: IEEE Standards Committee 754.
IEEE Standard for binary floating-point arithmetic, ANSI/IEEE Standard 754-1985.
Institute of Electrical and Electronics Engineers, New York, 1985.
26.: R. B. Kearfott.
Rigorous Global Search: Continuous Problems.
Kluwer, Dordrecht, Netherlands, 1996. MR 1422659 (97i:90003)
27.: C. Lawrence, J. L. Zhou, and A. L. Tits.
A C code for solving (large scale) constrained nonlinear (minimax) optimization problems, generating iterates satisfying all inequality constraints.
Technical Report TR-94-16r1, Institute for Systems Research, University of Maryland, 1997.
http://www.aemdesign.com/download-cfsqp/cfsqp-manual.pdf.
28.: S. McLaughlin.
KeplerCode: Computer resources for the Kepler and Dodecahedral Conjectures.
http://code.google.com/p/kepler-code/.
29.: D. J. Muder.
Putting the best face on a Voronoi polyhedron.
In Proceedings of the London Mathematical Society, volume 3/56, pages 329-348, 1988. MR 922659 (89e:52029)
30.: D. J. Muder.
A new bound on the local density of sphere packings.
In Discrete and Computational Geometry, volume 10, pages 351-375, 1993. MR 1243334 (94h:52041)
31.: T. Nipkow, G. Bauer, and P. Schultz.
Flyspeck I: Tame Graphs.
In U. Furbach and N. Shankar, editors, International Joint Conference on Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 21-35. Springer-Verlag, 2006. MR 2354670
32.: S. Obua.
Flyspeck II: The Basic Linear Programs.
Ph.D. thesis, Technische Universität München, 2008.
33.: L. Paulson.
Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science.
Springer-Verlag, 1994. MR 1313213 (96i:68072)
34.: W. H. Press et al.
Numerical Recipes in C, Chapter 20. Less-Numerical Algorithms.
Cambridge University Press, second edition, 1992. MR 1201159 (93i:65001b)
35.: C. A. Rogers.
The packing of equal spheres.
In Journal of the London Mathematical Society, volume 3/8, pages 609-620, 1958. MR 0102052 (21:847)
36.: R. Zumkeller.
Formal global optimisation with Taylor models.
In U. Furbach and N. Shankar, editors, International Joint Conference on Automated Reasoning, volume 4130 of Lecture Notes in Computer Science, pages 408-422. Springer-Verlag, 2006. MR 2361338
37.: R. Zumkeller.
Rigorous Global Optimization.
Ph.D. thesis, Ecole Polytechnique, 2008.

Retrieve articles in Journal of the American Mathematical Society with MSC (2010): 52C17

Thomas C. Hales
Affiliation: Department of Mathematics, University of Pittsburgh, 301 Thackeray Hall, Pittsburgh, Pennsylvania 15260
Email: hales@pitt.edu

Sean McLaughlin
Affiliation: Department of Mathematics, Carnegie Mellon University, Wean Hall 6113, Pittsburgh, Pennsylvania 15213
Email: seanmcl@gmail.com

DOI: 10.1090/S0894-0347-09-00647-X
PII: S 0894-0347(09)00647-X
Received by editor(s): November 1998
Posted: October 27, 2009
Copyright of article: Copyright 2009, American Mathematical Society
The copyright for this article reverts to public domain after 28 years from publication.

			Journals Home Search Author Info Subscribe Tech Support Help
ISSN: 1088-6834(e) ISSN: 0894-0347(p)

Previous issue \| Table of contents \| Next issue Articles in press \| Recently posted articles \| Most recent issue \| All issues Previous Article \| Next Article


	Comments: webmaster@ams.org © Copyright 2009, American Mathematical Society Privacy Statement		Search the AMS