Dense sphere packings. A blueprint for formal proofs
type: Item
instance of: scholarly article
zbMATH Open document ID: 1263.52001
author: Thomas C. Hales
publication date: 2012-06-22T00:00:00Z
Mathematics Subject Classification ID: 52-01
Mathematics Subject Classification ID: 52C17
zbMATH DE Number: 6049103
zbMATH Keywords: Kepler's conjecture
zbMATH Keywords: sphere packing
MaRDI profile type: Publication
title: Dense sphere packings. A blueprint for formal proofs
published in: London Mathematical Society Lecture Note Series
review text: The main goal of this interesting and unusual book is to present the famous proof of Kepler's conjecture, as previously obtained by the author, with a view towards the design of a formal proof to be constructed. In addition to being a fascinating account of the great problem and its solution, it also serves as a blueprint for a large scale project, aiming to verify every step of the proof of Kepler's conjecture on a computer. While culminating in some extremely non-trivial mathematics, it is also an excellent introduction to the subject for anyone with a curiosity.NEWLINENEWLINEThe first part of the book is devoted to a brief historical overview of the subject of sphere packing, starting out with its origin in the work of mathematicians of antiquity, then through Harriot and Kepler, Newton and Gregory, Gauss, Thue, and all the way to the linear programming techniques of the present day.NEWLINENEWLINEThe second part lays down the mathematical foundations needed for the arguments to follow. The author first presents a careful development of basic trigonometric techniques and volume computations. He then introduces the notion of a hypermap, an abstraction of the concept of plane graph and carefully discusses its properties. Finally the topology and geometry of fans and polyhedra are discussed.NEWLINENEWLINEPart three is the core of the book, which embarks on the actual packing constructions and Kepler's conjecture. The discussion starts out with the important objects of the packing theory, such as Voronoi cells, Delaunay and Rogers decompositions, and Marchal cells. A conjecture of Marchal on FCC-compatibility of saturated packings is presented, and its variant is later proved in this book. Properties of Marchal cell decomposition are then investigated. The author's proof of Kepler's conjecture employs a number of difficult technical estimates, which are also presented in the third part of the book by investigating the properties of local fans. Finally, the proof of th…
reviewed by: Lenny Fukshansky
description: scientific article; zbMATH DE number 6049103