Remote Access Journal of the American Mathematical Society
Green Open Access

Journal of the American Mathematical Society

ISSN 1088-6834(online) ISSN 0894-0347(print)



The dodecahedral conjecture

Authors: Thomas C. Hales and Sean McLaughlin
Journal: J. Amer. Math. Soc. 23 (2010), 299-344
MSC (2010): Primary 52C17
Published electronically: October 27, 2009
Supplement: Additional materials posted with this article.
MathSciNet review: 2601036
Full-text PDF Free Access

Abstract | References | Similar Articles | Additional Information

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 [Enhancements On Off] (What's this?)

  • 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
  • Károly Bezdek, Isoperimetric inequalities and the dodecahedral conjecture, Internat. J. Math. 8 (1997), no. 6, 759–780. MR 1470853, DOI
  • 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
  • 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
  • George E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, Automata theory and formal languages (Second GI Conf., Kaiserslautern, 1975), Springer, Berlin, 1975, pp. 134–183. Lecture Notes in Comput. Sci., Vol. 33. MR 0403962
  • L. Fejes, Über die dichteste Kugellagerung, Math. Z. 48 (1943), 676–684 (German). MR 9129, DOI
  • L. Fejes Tóth, Regular figures, A Pergamon Press Book, The Macmillan Co., New York, 1964. MR 0165423
  • László Fejes Tóth, Lagerungen in der Ebene auf der Kugel und im Raum, Springer-Verlag, Berlin-New York, 1972 (German). Zweite verbesserte und erweiterte Auflage; Die Grundlehren der mathematischen Wissenschaften, Band 65. 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.
  • T. C. Hales. The Flyspeck Fact Sheet, 2003 (revised 2007).
  • Thomas C. Hales, The status of the Kepler conjecture, Math. Intelligencer 16 (1994), no. 3, 47–58. MR 1281754, DOI
  • T. C. Hales, Sphere packings. I, Discrete Comput. Geom. 17 (1997), no. 1, 1–51. MR 1418278, DOI
  • 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
  • T. C. Hales. The Flyspeck Project, 2007.
  • 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
  • T. C. Hales and S. McLaughlin. A proof of the dodecahedral conjecture (1998 version).
  • T. C. Hales and S. McLaughlin. A proof of the dodecahedral conjecture (2002 version).
  • E. Harshbarger. Saturated packings and Voronoi cells, 1996.
  • 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
  • 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
  • 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
  • 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.
  • S. McLaughlin. KeplerCode: Computer resources for the Kepler and Dodecahedral Conjectures.
  • 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
  • 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
  • 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
  • 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
  • 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
  • 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
  • R. Zumkeller. Rigorous Global Optimization. Ph.D. thesis, Ecole Polytechnique, 2008.

Similar Articles

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

Retrieve articles in all journals with MSC (2010): 52C17

Additional Information

Thomas C. Hales
Affiliation: Department of Mathematics, University of Pittsburgh, 301 Thackeray Hall, Pittsburgh, Pennsylvania 15260

Sean McLaughlin
Affiliation: Department of Mathematics, Carnegie Mellon University, Wean Hall 6113, Pittsburgh, Pennsylvania 15213

Received by editor(s): November 19, 1998
Published electronically: October 27, 2009
Article copyright: © Copyright 2009 American Mathematical Society
The copyright for this article reverts to public domain 28 years after publication.