Remote Access Bulletin of the American Mathematical Society

Bulletin of the American Mathematical Society

ISSN 1088-9485(online) ISSN 0273-0979(print)

Book Review

The AMS does not provide abstracts of book reviews. You may download the entire review from the links below.


Full text of review: PDF   This review is available free of charge.
Book Information:

Author: Thomas C. Hales
Title: Dense sphere packings: a blueprint for formal proofs
Additional book information: London Mathematical Society Lecture Note Series, Vol. 400, Cambridge University Press, Cambridge, 2012, xiv+271 pp., ISBN 978-0-521-61770-3

References [Enhancements On Off] (What's this?)

  • [1] J. Barlow, Probable nature of the internal symmetry of crystals, Nature 29 (1883), 186-188.
  • [2] 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 (2001b:52033), https://doi.org/10.1515/crll.2000.001
  • [3] J. H. Conway and N. J. A. Sloane, Sphere packings, lattices and groups, With additional contributions by E. Bannai, R. E. Borcherds, J. Leech, S. P. Norton, A. M. Odlyzko, R. A. Parker, L. Queen and B. B. Venkov, 3rd ed., Grundlehren der Mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 290, Springer-Verlag, New York, 1999. MR 1662447 (2000b:11077)
  • [4] László Fejes-Tóth, Über die dichteste Kugellagerung, Math. Z. 48 (1943), 676-684 (German). MR 0009129 (5,106f)
  • [5] L. 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 (50 #5603)
  • [6] L. Fejes-Tóth, Regular figures, A Pergamon Press Book, The Macmillan Co., New York, 1964. MR 0165423 (29 #2705)
  • [7] L. Fejes-Tóth, Remarks on a theorem of R. M. Robinson, Studia Sci. Math. Hungar. 4 (1969), 441-445. MR 0254744 (40 #7951)
  • [8] L. Fejes-Tóth, Research problems, Period. Math. Hungar. 20 (1989), no. 1, 89-91. MR 1553649, https://doi.org/10.1007/BF01849507
  • [9] G. Gonthier, A. Asparti, J. Avigad, et al., A machine-checked proof of the odd order theorem, pp. 163-179 in: Interactive Theorem Proving, Lecture Notes in Compter Science 7998, Springer: Heidelberg 2013.
  • [10] Thomas C. Hales, Sphere packings I, Discrete Comput. Geom. 17 (1997), no. 1, 1-51. MR 1418278 (97k:52025)
  • [11] Thomas C. Hales, Sphere packings II, Discrete Comput. Geom. 18 (1997), no. 2, 135-149. MR 1455511 (98h:52033)
  • [12] Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065-1185. MR 2179728 (2006g:52029), https://doi.org/10.4007/annals.2005.162.1065
  • [13] Thomas C. Hales, Historical overview of the Kepler conjecture, Discrete Comput. Geom. 36 (2006), no. 1, 5-20. MR 2229657 (2007d:52021), https://doi.org/10.1007/s00454-005-1210-2
  • [14] Thomas C. Hales and Samuel P. Ferguson, A formulation of the Kepler conjecture, Discrete Comput. Geom. 36 (2006), no. 1, 21-69. MR 2229658 (2007d:52022), https://doi.org/10.1007/s00454-005-1211-1
  • [15] Thomas C. Hales, Sphere packings. III. Extremal cases, Discrete Comput. Geom. 36 (2006), no. 1, 71-110. MR 2229659 (2007d:52023), https://doi.org/10.1007/s00454-005-1212-0
  • [16] Thomas C. Hales, Sphere packings. IV. Detailed bounds, Discrete Comput. Geom. 36 (2006), no. 1, 111-166. MR 2229660 (2007d:52024), https://doi.org/10.1007/s00454-005-1213-z
  • [17] Samuel P. Ferguson, Sphere packings. V. Pentahedral prisms, Discrete Comput. Geom. 36 (2006), no. 1, 167-204. MR 2229661 (2007d:52025), https://doi.org/10.1007/s00454-005-1214-y
  • [18] Thomas C. Hales, Sphere packings. VI. Tame graphs and linear programs, Discrete Comput. Geom. 36 (2006), no. 1, 205-265. MR 2229662 (2007d:52026), https://doi.org/10.1007/s00454-005-1215-x
  • [19] Thomas C. Hales, The strong dodecahedral conjecture and Fejes-Tóth's conjecture on sphere packings with kissing number twelve, Discrete geometry and optimization, Fields Inst. Commun., vol. 69, Springer, New York, 2013, pp. 121-132. MR 3156780, https://doi.org/10.1007/978-3-319-00200-2_8
  • [20] T. C. Hales, Developments in formal proofs, Séminaire BOURBAKI, 2013-2014, No. 1086, 23 pages, arXiv:1408.6474v1.
  • [21] T. C. Hales, The Flyspeck project, http://code.google.com/p/flyspeck.
  • [22] T. Hales, private communication.
  • [23] T. Hales, M. Adams, G. Bauer, Dang Tat Dat, J. Harrison, Hoang Le Truong, C. Kaliszyk, V. Magron, S. McLauglin, Nguyen Tat Thang, Nguyen Quang Truong, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, Ta Thi Hoai An, Tran Nam Thung, Trieu Thi Diep, J. Urban, Vu Khac Ky, R. Zumkeller, A Formal Proof of the Kepler Conjecture, arXiv:1501.02155v1.
  • [24] Thomas C. Hales and Samuel P. Ferguson, A formulation of the Kepler conjecture, Discrete Comput. Geom. 36 (2006), no. 1, 21-69. MR 2229658 (2007d:52022), https://doi.org/10.1007/s00454-005-1211-1
  • [25] Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller, A revision of the proof of the Kepler conjecture, Discrete Comput. Geom. 44 (2010), no. 1, 1-34. MR 2639816 (2012h:52044), https://doi.org/10.1007/s00454-009-9148-4
  • [26] Thomas C. Hales and Sean McLaughlin, The dodecahedral conjecture, J. Amer. Math. Soc. 23 (2010), no. 2, 299-344. MR 2601036 (2011d:52037), https://doi.org/10.1090/S0894-0347-09-00647-X
  • [27] John Harrison, HOL Light: an overview, Theorem proving in higher order logics, Lecture Notes in Comput. Sci., vol. 5674, Springer, Berlin, 2009, pp. 60-66. MR 2550931, https://doi.org/10.1007/978-3-642-03359-9_4
  • [28] John Harrison, The HOL Light theory of Euclidean space, J. Automat. Reason. 50 (2013), no. 2, 173-190. MR 3016800, https://doi.org/10.1007/s10817-012-9250-9
  • [29] D. Hilbert, Mathematische Probleme, Göttinger Nachrichten, 1900, pp. 253-297; Archiv für Mathematik und Physik 1 (1901), 44-63 and 213-237. English Translation: Mathematical Problems, Bull. Amer. Math. Soc. 8 (1902), 437-479.
  • [30] D. Hilbert, Grundlagen der Geometrie, Tenth edition. B. G. Teubner: Stuttgart English version: Foundations of Geometry, Leo Ungar, Translator/ Revised by Paul Bernays. Open Court Publishing Company, 1971.
  • [31] J. Kepler, A New Year's Gift, or, On the Six-Cornered Snowflake (Latin), Francofurti ad Moenum apud Godfefridum Tampach, 1611.
  • [32] J. C. Lagarias, Bounds for local density of sphere packings and the Kepler conjecture, Discrete Comput. Geom. 27 (2002), no. 2, 165-193. MR 1880936 (2002k:52027), https://doi.org/10.1007/978-1-4614-1129-1_2
  • [33] Jeffrey C. Lagarias, The Kepler conjecture and its proof, The Kepler conjecture, Springer, New York, 2011, pp. 3-26. MR 3050907, https://doi.org/10.1007/978-1-4614-1129-1_1
  • [34] Christian Marchal, Study of the Kepler's conjecture: the problem of the closest packing, Math. Z. 267 (2011), no. 3-4, 737-765. MR 2776056 (2012b:52032), https://doi.org/10.1007/s00209-009-0644-2
  • [35] Sean McLaughlin, An interpretation of Isabelle/HOL in HOL Light, Automated reasoning, Lecture Notes in Comput. Sci., vol. 4130, Springer, Berlin, 2006, pp. 192-204. MR 2354684, https://doi.org/10.1007/11814771_18
  • [36] Laura I. Meikle and Jacques D. Fleuriot, Formalizing Hilbert's Grundlagen in Isabelle/Isar, Theorem proving in higher order logics, Lecture Notes in Comput. Sci., vol. 2758, Springer, Berlin, 2003, pp. 319-334. MR 2077104, https://doi.org/10.1007/10930755_21
  • [37] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel, Isabelle/HOL, A proof assistant for higher-order logic, Lecture Notes in Computer Science, vol. 2283, Springer-Verlag, Berlin, 2002. MR 1949173 (2003m:68120)
  • [38] C. A. Rogers, The packing of equal spheres, Proc. London Math. Soc. (3) 8 (1958), 609-620. MR 0102052 (21 #847)

Review Information:

Reviewer: Jeffrey C. Lagarias
Affiliation: University of Michigan
Email: lagarias@umich.edu
Journal: Bull. Amer. Math. Soc. 53 (2016), 159-166
MSC (2010): Primary 52C17, 68T15; Secondary 51M20, 51Mxx, 65Kxx, 90C05, 90C26
DOI: https://doi.org/10.1090/bull/1502
Published electronically: June 9, 2015
Review copyright: © Copyright 2015 American Mathematical Society
American Mathematical Society