Dense sphere packings. A blueprint for formal proofs (Q2892718)

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 the conjecture is presented by a detailed study of the hypermaps.NEWLINENEWLINEThis is an important book, which presents the mathematics behind the technical proof of Kepler's conjecture, as well as several other related big problems in discrete geometry in a completely self-contained way. The book is beautifully written and is full of interesting historical notes. Moreover, each chapter is equipped with a very helpful summary, and many technical arguments are accompanied by a conceptual informal discussion. The book also features a detailed index and a nice bibliography. It is bound to become an indispensable resource for anyone wishing to study Kepler's conjecture.