The dodecahedral conjecture

Hales, Thomas; McLaughlin, Sean

doi:10.1090/S0894-0347-09-00647-X

The dodecahedral conjecture
HTML articles powered by AMS MathViewer

by Thomas C. Hales and Sean McLaughlin

J. Amer. Math. Soc. 23 (2010), 299-344

DOI: https://doi.org/10.1090/S0894-0347-09-00647-X

Published electronically: October 27, 2009

PDF | Request permission

Supplement: Additional materials posted with this article.

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.

References

Götz Alefeld and Jürgen Herzberger, Introduction to interval computations, Computer Science and Applied Mathematics, Academic Press, Inc. [Harcourt Brace Jovanovich, Publishers], New York, 1983. Translated from the German by Jon Rokne. MR 733988
G. Bauer. Formalizing Plane Graph Theory – Towards a Formalized Proof of the Kepler Conjecture. Ph.D. thesis, Technische Universität München, 2006.
Yves Bertot and Pierre Castéran, Interactive theorem proving and program development, Texts in Theoretical Computer Science. An EATCS Series, Springer-Verlag, Berlin, 2004. Coq’Art: the calculus of inductive constructions; With a foreword by Gérard Huet and Christine Paulin-Mohring. MR 2229784, DOI 10.1007/978-3-662-07964-5
Károly Bezdek, Isoperimetric inequalities and the dodecahedral conjecture, Internat. J. Math. 8 (1997), no. 6, 759–780. MR 1470853, DOI 10.1142/S0129167X9700038X
Károly Bezdek, On a stronger form of Rogers’s lemma and the minimum surface area of Voronoi cells in unit ball packings, J. Reine Angew. Math. 518 (2000), 131–143. MR 1739407, DOI 10.1515/crll.2000.001
Richard H. Byrd, Jorge Nocedal, and Richard A. Waltz, KNITRO: An integrated package for nonlinear optimization, Large-scale nonlinear optimization, Nonconvex Optim. Appl., vol. 83, Springer, New York, 2006, pp. 35–59. MR 2194566, DOI 10.1007/0-387-30065-1_{4}
George E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Automata theory and formal languages (Second GI Conf., Kaiserslautern, 1975), Lecture Notes in Comput. Sci., Vol. 33, Springer, Berlin, 1975, pp. 134–183. MR 0403962
L. Fejes, Über die dichteste Kugellagerung, Math. Z. 48 (1943), 676–684 (German). MR 9129, DOI 10.1007/BF01180035
L. Fejes Tóth, Regular figures, A Pergamon Press Book, The Macmillan Company, New York, 1964. MR 0165423
László Fejes Tóth, Lagerungen in der Ebene auf der Kugel und im Raum, Die Grundlehren der mathematischen Wissenschaften, Band 65, Springer-Verlag, Berlin-New York, 1972 (German). Zweite verbesserte und erweiterte Auflage. MR 0353117
G. Gonthier. A computer-checked proof of the four colour theorem. Unpublished manuscript, 2005.
T. Hales and S. McLaughlin. An appendix to the dodecahedral conjecture. http://www.ams.org/jams.
T. C. Hales. The Flyspeck Fact Sheet, 2003 (revised 2007). http://code.google.com/p/flyspeck/wiki/FlyspeckFactSheet.
Thomas C. Hales, The status of the Kepler conjecture, Math. Intelligencer 16 (1994), no. 3, 47–58. MR 1281754, DOI 10.1007/BF03024356
T. C. Hales, Sphere packings. I, Discrete Comput. Geom. 17 (1997), no. 1, 1–51. MR 1418278, DOI 10.1007/BF02770863
Thomas C. Hales, Some algorithms arising in the proof of the Kepler conjecture, Discrete and computational geometry, Algorithms Combin., vol. 25, Springer, Berlin, 2003, pp. 489–507. MR 2038488, DOI 10.1007/978-3-642-55566-4_{2}2
T. C. Hales. The Flyspeck Project, 2007. http://code.google.com/p/flyspeck.
Thomas C. Hales and Samuel P. Ferguson, A formulation of the Kepler conjecture, Discrete Comput. Geom. 36 (2006), no. 1, 21–69. MR 2229658, DOI 10.1007/s00454-005-1211-1
T. C. Hales and S. McLaughlin. A proof of the dodecahedral conjecture (1998 version). http://arxiv.org/abs/math/9811079v1.
T. C. Hales and S. McLaughlin. A proof of the dodecahedral conjecture (2002 version). http://arxiv.org/abs/math/9811079v2.
E. Harshbarger. Saturated packings and Voronoi cells, 1996. http://www.ericharshbarger.org/voronoi.html.
J. F. Hart et al. Computer Approximations. John Wiley & Sons, 1968.
Lars Hörmander, The analysis of linear partial differential operators. II, Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 257, Springer-Verlag, Berlin, 1983. Differential operators with constant coefficients. MR 705278, DOI 10.1007/978-3-642-96750-4
Wu-Yi Hsiang, On the sphere packing problem and the proof of Kepler’s conjecture, Internat. J. Math. 4 (1993), no. 5, 739–831. MR 1245351, DOI 10.1142/S0129167X93000364
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.
R. Baker Kearfott, Rigorous global search: continuous problems, Nonconvex Optimization and its Applications, vol. 13, Kluwer Academic Publishers, Dordrecht, 1996. MR 1422659, DOI 10.1007/978-1-4757-2495-0
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.
S. McLaughlin. KeplerCode: Computer resources for the Kepler and Dodecahedral Conjectures. http://code.google.com/p/kepler-code/.
Douglas J. Muder, Putting the best face on a Voronoĭ polyhedron, Proc. London Math. Soc. (3) 56 (1988), no. 2, 329–348. MR 922659, DOI 10.1112/plms/s3-56.2.329
Douglas J. Muder, A new bound on the local density of sphere packings, Discrete Comput. Geom. 10 (1993), no. 4, 351–375. MR 1243334, DOI 10.1007/BF02573984
Tobias Nipkow, Gertrud Bauer, and Paula Schultz, Flyspeck. I. Tame graphs, Automated reasoning, Lecture Notes in Comput. Sci., vol. 4130, Springer, Berlin, 2006, pp. 21–35. MR 2354670, DOI 10.1007/11814771_{4}
S. Obua. Flyspeck II: The Basic Linear Programs. Ph.D. thesis, Technische Universität München, 2008.
Lawrence C. Paulson, Isabelle, Lecture Notes in Computer Science, vol. 828, Springer-Verlag, Berlin, 1994. A generic theorem prover; With contributions by Tobias Nipkow. MR 1313213, DOI 10.1007/BFb0030541
William H. Press, Saul A. Teukolsky, William T. Vetterling, and Brian P. Flannery, Numerical recipes in C, 2nd ed., Cambridge University Press, Cambridge, 1992. The art of scientific computing. MR 1201159
C. A. Rogers, The packing of equal spheres, Proc. London Math. Soc. (3) 8 (1958), 609–620. MR 102052, DOI 10.1112/plms/s3-8.4.609
Roland Zumkeller, Formal global optimisation with Taylor models, Automated reasoning, Lecture Notes in Comput. Sci., vol. 4130, Springer, Berlin, 2006, pp. 408–422. MR 2361338, DOI 10.1007/11814771_{3}5
R. Zumkeller. Rigorous Global Optimization. Ph.D. thesis, Ecole Polytechnique, 2008.