Dr. Thomas Hales awarded Senior Berwick Prize

Professor Thomas Hales of the University of Pittsburgh is awarded a Senior Berwick Prize in recognition of his book: ‘Dense sphere packings. A blueprint for formal proofs’ (London Mathematical Society Lecture Note Series, 400. Cambridge University Press, Cambridge, 2012. xiv+271 pp. ISBN: 978-0-521-61770-3).
 
The 400-year-old Kepler conjecture asserts that no packing of congruent balls in three dimensions can have a density exceeding the familiar pyramid-shaped cannonball arrangement. In this work, a new proof of the conjecture is presented that makes it accessible for the first time to a broad mathematical audience. It also presents solutions to other previously unresolved conjectures in discrete geometry, including the strong dodecahedral conjecture on the smallest surface area of a Voronoi cell in a sphere packing. The book has been used as a blueprint for a large-scale formal computer proof project, which checked every logical inference of the proof of Kepler’s conjecture. Hales’ book continues the programme initiated in his highly-cited 2005 Annals of Mathematics paper: A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185.),  and presents a beautiful proof, in a clear, thoughtful and engaging manner.  
 
Not only is formal proof a topic of continued and growing interest, spurred on by the developments around Homotopy Type Theory (and Vladimir Voevodsky's untimely passing in September 2017), but also sphere packings in general are back in the news following the resolution by Maryna Viazovska in 2016 of the corresponding problem in dimension 8, and by Viazovska and collaborators in dimension 24 in 2017.
 
Apart from the obvious historical importance of Kepler’s conjecture, the increasing complexity of mathematical proofs and the increasing use of computers to deliver mathematical results make it inevitable that formal methods have come to play a key role in supporting mathematical reasoning and ensuring correctness. Hales’ computer-assisted proof of the Kepler conjecture presented in this book is therefore an important landmark in this respect.