Bulletin of the American Mathematical Society

MathSciNet review: 3443950
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

J. Barlow, Probable nature of the internal symmetry of crystals, Nature 29 (1883), 186–188.

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

J. H. Conway and N. J. A. Sloane, Sphere packings, lattices and groups, 3rd ed., Grundlehren der mathematischen Wissenschaften [Fundamental Principles of Mathematical Sciences], vol. 290, Springer-Verlag, New York, 1999. 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. MR 1662447, DOI 10.1007/978-1-4757-6568-7

L. Fejes, Über die dichteste Kugellagerung, Math. Z. 48 (1943), 676–684 (German). MR 9129, DOI 10.1007/BF01180035

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

L. Fejes Tóth, Regular figures, A Pergamon Press Book, The Macmillan Company, New York, 1964. MR 0165423

L. Fejes Tóth, Remarks on a theorem of R. M. Robinson, Studia Sci. Math. Hungar. 4 (1969), 441–445. MR 254744

L. Fejes Tóth, Research problems, Period. Math. Hungar. 20 (1989), no. 1, 89–91. MR 1553649, DOI 10.1007/BF01849507

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.

T. C. Hales, Sphere packings. I, Discrete Comput. Geom. 17 (1997), no. 1, 1–51. MR 1418278, DOI 10.1007/BF02770863

T. C. Hales, Sphere packings. II, Discrete Comput. Geom. 18 (1997), no. 2, 135–149. MR 1455511, DOI 10.1007/PL00009312

Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185. MR 2179728, DOI 10.4007/annals.2005.162.1065

Thomas C. Hales, Historical overview of the Kepler conjecture, Discrete Comput. Geom. 36 (2006), no. 1, 5–20. MR 2229657, DOI 10.1007/s00454-005-1210-2

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

Thomas C. Hales, Sphere packings. III. Extremal cases, Discrete Comput. Geom. 36 (2006), no. 1, 71–110. MR 2229659, DOI 10.1007/s00454-005-1212-0

Thomas C. Hales, Sphere packings. IV. Detailed bounds, Discrete Comput. Geom. 36 (2006), no. 1, 111–166. MR 2229660, DOI 10.1007/s00454-005-1213-z

Samuel P. Ferguson, Sphere packings. V. Pentahedral prisms, Discrete Comput. Geom. 36 (2006), no. 1, 167–204. MR 2229661, DOI 10.1007/s00454-005-1214-y

Thomas C. Hales, Sphere packings. VI. Tame graphs and linear programs, Discrete Comput. Geom. 36 (2006), no. 1, 205–265. MR 2229662, DOI 10.1007/s00454-005-1215-x

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, DOI 10.1007/978-3-319-00200-2_{8}

T. C. Hales, Developments in formal proofs, Séminaire BOURBAKI, 2013–2014, No. 1086, 23 pages, arXiv:1408.6474v1.

T. C. Hales, The Flyspeck project, http://code.google.com/p/flyspeck.

T. Hales, private communication.

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.

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

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, DOI 10.1007/s00454-009-9148-4

Thomas C. Hales and Sean McLaughlin, The dodecahedral conjecture, J. Amer. Math. Soc. 23 (2010), no. 2, 299–344. MR 2601036, DOI 10.1090/S0894-0347-09-00647-X

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, DOI 10.1007/978-3-642-03359-9_{4}

John Harrison, The HOL light theory of Euclidean space, J. Automat. Reason. 50 (2013), no. 2, 173–190. MR 3016800, DOI 10.1007/s10817-012-9250-9

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.

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.

J. Kepler, A New Year’s Gift, or, On the Six-Cornered Snowflake (Latin), Francofurti ad Moenum apud Godfefridum Tampach, 1611.

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, DOI 10.1007/978-1-4614-1129-1_{2}

Jeffrey C. Lagarias, The Kepler conjecture and its proof, The Kepler conjecture, Springer, New York, 2011, pp. 3–26. MR 3050907, DOI 10.1007/978-1-4614-1129-1_{1}

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, DOI 10.1007/s00209-009-0644-2

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, DOI 10.1007/11814771_{1}8

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, DOI 10.1007/10930755_{2}1

Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel, Isabelle/HOL, Lecture Notes in Computer Science, vol. 2283, Springer-Verlag, Berlin, 2002. A proof assistant for higher-order logic. MR 1949173, DOI 10.1007/3-540-45949-9

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

• J. Barlow, Probable nature of the internal symmetry of crystals, Nature 29 (1883), 186–188.
• 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), DOI 10.1515/crll.2000.001
• 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), DOI 10.1007/978-1-4757-6568-7
• László Fejes-Tóth, Über die dichteste Kugellagerung, Math. Z. 48 (1943), 676–684 (German). MR 0009129 (5,106f)
• 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)
• L. Fejes-Tóth, Regular figures, A Pergamon Press Book, The Macmillan Co., New York, 1964. MR 0165423 (29 \#2705)
• L. Fejes-Tóth, Remarks on a theorem of R. M. Robinson, Studia Sci. Math. Hungar. 4 (1969), 441–445. MR 0254744 (40 \#7951)
• L. Fejes-Tóth, Research problems, Period. Math. Hungar. 20 (1989), no. 1, 89–91. MR 1553649, DOI 10.1007/BF01849507
• 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.
• Thomas C. Hales, Sphere packings I, Discrete Comput. Geom. 17 (1997), no. 1, 1–51. MR 1418278 (97k:52025)
• Thomas C. Hales, Sphere packings II, Discrete Comput. Geom. 18 (1997), no. 2, 135–149. MR 1455511 (98h:52033)
• Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185. MR 2179728 (2006g:52029), DOI 10.4007/annals.2005.162.1065
• Thomas C. Hales, Historical overview of the Kepler conjecture, Discrete Comput. Geom. 36 (2006), no. 1, 5–20. MR 2229657 (2007d:52021), DOI 10.1007/s00454-005-1210-2
• 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), DOI 10.1007/s00454-005-1211-1
• Thomas C. Hales, Sphere packings. III. Extremal cases, Discrete Comput. Geom. 36 (2006), no. 1, 71–110. MR 2229659 (2007d:52023), DOI 10.1007/s00454-005-1212-0
• Thomas C. Hales, Sphere packings. IV. Detailed bounds, Discrete Comput. Geom. 36 (2006), no. 1, 111–166. MR 2229660 (2007d:52024), DOI 10.1007/s00454-005-1213-z
• Samuel P. Ferguson, Sphere packings. V. Pentahedral prisms, Discrete Comput. Geom. 36 (2006), no. 1, 167–204. MR 2229661 (2007d:52025), DOI 10.1007/s00454-005-1214-y
• Thomas C. Hales, Sphere packings. VI. Tame graphs and linear programs, Discrete Comput. Geom. 36 (2006), no. 1, 205–265. MR 2229662 (2007d:52026), DOI 10.1007/s00454-005-1215-x
• 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, DOI 10.1007/978-3-319-00200-2_8
• T. C. Hales, Developments in formal proofs, Séminaire BOURBAKI, 2013–2014, No. 1086, 23 pages, arXiv:1408.6474v1.
• T. C. Hales, The Flyspeck project, http://code.google.com/p/flyspeck.
• T. Hales, private communication.
• 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.
• 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), DOI 10.1007/s00454-005-1211-1
• 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), DOI 10.1007/s00454-009-9148-4
• Thomas C. Hales and Sean McLaughlin, The dodecahedral conjecture, J. Amer. Math. Soc. 23 (2010), no. 2, 299–344. MR 2601036 (2011d:52037), DOI 10.1090/S0894-0347-09-00647-X
• 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, DOI 10.1007/978-3-642-03359-9_4
• John Harrison, The HOL Light theory of Euclidean space, J. Automat. Reason. 50 (2013), no. 2, 173–190. MR 3016800, DOI 10.1007/s10817-012-9250-9
• 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.
• 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.
• J. Kepler, A New Year’s Gift, or, On the Six-Cornered Snowflake (Latin), Francofurti ad Moenum apud Godfefridum Tampach, 1611.
• 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), DOI 10.1007/978-1-4614-1129-1_2
• Jeffrey C. Lagarias, The Kepler conjecture and its proof, The Kepler conjecture, Springer, New York, 2011, pp. 3–26. MR 3050907, DOI 10.1007/978-1-4614-1129-1_1
• 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), DOI 10.1007/s00209-009-0644-2
• 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, DOI 10.1007/11814771_18
• 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, DOI 10.1007/10930755_21
• 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), DOI 10.1007/3-540-45949-9
• C. A. Rogers, The packing of equal spheres, Proc. London Math. Soc. (3) 8 (1958), 609–620. MR 0102052 (21 \#847)