References
Published online by Cambridge University Press: 05 October 2012
Summary
A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.
- Type
- Chapter
- Information
- Dense Sphere PackingsA Blueprint for Formal Proofs, pp. 261 - 263Publisher: Cambridge University PressPrint publication year: 2012
References
[1] On the heaven. translated by , http://classics.mit.edu/Aristotle/heavens.html, 350BC.
[2] . A Course in Convexity, volume 54 of Graduate Studies in Mathematics. American Mathematical Society, 2002.
[3] and , editors. Thomas Harriot's Doctrine of Triangular Numbers: the ‘Magisteria Magna’. European Math. Soc., 2008.
[4] . On a stronger form of Rogers' lemma and the minimum surface area of Voronoi cells in unit ball packings. J. Reine Angew. Math., 518:131–143, 2000.Google Scholar
[5] and . Finding the best face on a Voronoi polyhedron – the strong dodecahedral conjecture revisited. Monatshefte für Mathematik, 145:145–2006, 2005.Google Scholar
[6] . Computational Real Algebraic Geometry. CRC Press, 1997.
[7] . Elements of Sets. Addison-Wesley, Boston MA, 1968.
[8] . Packing pennies in the plane, an illustrated proof of Kepler's conjecture in 2d. AMS Feature Column Archive, http://www.ams.org/featurecolumn/archive/cass1.html, December 2000.
[9] and . What are all the best sphere packings in low dimensions?DCG, 13:13–403, 1995.Google Scholar
[10] and . Logicomix An Epic Search for Truth. Worzalla Publishing, 2009.
[11] . Variae speculationes super area triangulorum sphaericorum. N. Acta Ac. Petrop., pages 47–62, 1797. E698 (Erneström index).
[12] . Lagerungen in der Ebene auf der Kugel und im Raum. Springer-Verlag, Berlin-New York, first edition, 1953.
[13] . Introduction to Toric Varieties. Princeton University Press, Princeton NJ, 1993.
[14] . Untersuchungen über die Eigenscahften der positiven ternären quadratischen Formen von Ludwig August Seber. Göttingische gelehrte Anzeigen, July 1831. also published in J. Reine Angew. Math. 20 (1840), 312–320, and Werke, vol. 2, Königliche Gesellschaft der Wissenschaften, Göttingen, 1876, 188–196.
[15] . A computer-checked proof of the four colour theorem. Unpublished manuscript, 2005.
[16] . Formal proof – the four colour theorem. Notices of the AMS, 55(11):1382–1393, December 2008.Google Scholar
[17] . The art of worldly wisdom. Frederick Ungar Publishing, New York NY, 1967.
[18] . The sphere packing problem. In Journal of Computational and Applied Math, volume 44, pages 41–76, 1992.Google Scholar
[20] . An overview of the Kepler conjecture. Discrete and Computational Geometry, 36(1):5–20, 2006.Google Scholar
[21] . The Flyspeck Project, 2012. http://code.google.com/p/flyspeck.
[22] and . The Kepler conjecture. Discrete and Computational Geometry, 36(1):1–269, 2006.Google Scholar
[23] and . A proof of the dodecahedral conjecture. Journal of the AMS, 23:23–344, 2010. http://arxiv.org/abs/math/9811079.Google Scholar
[24] , , , , , and . A revision of the proof of the Kepler Conjecture. DCG, 2009.
[25] . Formalizing an analytic proof of the prime number theorem. Journal of Automated Reasoning, 43:43–261, 2009.Google Scholar
[26] . The HOL Light theorem prover, 2010. http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html.
[27] . Atomism in England from Hariot to Newton. Clarendon Press, Oxford, 1966.
[28] . The Six-cornered snowflake. Oxford Clarendon Press, 1966. forward by .
[29] . You are not a gadget. Alfred A. Knopf, New York, 2010.
[30] . The problem of the thirteen spheres. In Mathematical Gazette, pages 22–23, February 1956.
[31] . Study of the Kepler's conjecture: the problem of the closest packing. Mathematische Zeitschrift, December 2009.
[32] and . The strong thirteen spheres problem. preprint http://arxiv.org/abs/1002.1439, February 2010.
[33] , , and . Flyspeck I: Tame Graphs. In and , editors, International Joint Conference on Automated Reasoning, volume 4130 of Lect. Notes in Comp. Sci., pages 21–35. Springer-Verlag, 2006.
[34] . Proving bounds for real linear programs in Isabelle/HOL. In and , editors, Theorem Proving in Higher Order Logics, volume 3603 of Lect. Notes in Comp. Sci., pages 227–244. Springer-Verlag, 2005.
[35] , January 2000. private communication.
[36] . The packing of equal spheres. Journal of the London Mathematical Society, 3/8:8–620, 1958.Google Scholar
[37] and . Auf welcher Kugel haben 5, 6, 7, oder 9 Punkte mit Mindestabstand Eins Platz. Math. Annalen, 123:123–124, 1951.Google Scholar
[39] . Thomas Harriot: a biography. Oxford, 1983.
[40] . The Āryabhaṭīya of Āryabhaṭa with the Commentary of Bhāskara I and Someśvara. New Delhi: Indian National Science Academy, 1976.
[41] and . Efficient formal verification of bounds of linear programs, volume 6824 of LNCS, pages 123–132. Springer-Verlag, 2011.
[42] . Joel on Software. Apress, 2004.
[43] . Kepler's Conjecture: How Some of the Greatest Minds in History Helped to Solve one of the Oldest Math Problems in the Worlds. John Wiley and Sons, New York NY, 2003.
[44] . A decision method for elementary algebra and geometry. University of California Press, Berkeley and Los Angeles, Calif., 1951. 2nd ed.
[45] . Om nogle geometrisk taltheoretiske theoremer. Forandlingerneved de Skandinaviske Naturforskeres, 14:14–353, 1892.Google Scholar
[46] . über die dichteste Zusammenstellung von kongruenten Kreisen in der Ebene. Christinia Vid. Selsk. Skr., 1:1–9, 1910.Google Scholar
[47] . Graph Theory. Encyclopedia of Mathematics and Its Applications. Addison-Wesley Publishing, 1984.
[48] . Convexity. Oxford University Press, 1994.
[49] . Jordan curve theorem. http://www.cs.ru.nl/~freek/jordan/index.html, referenced 2010.
[50] . Formalizing 100 theorems. http://www.cs.ru.nl/~freek/100/, referenced 2012.