Prof. Thomas Hales - Lessons learned from the Formal Proof of the Kepler Conjecture

Professor Thomas Hales, Mellon Professor at the University of Pittsburgh, gives a lecture entitled "Lessons learned from the Formal Proof of the Kepler Conjecture".
The Kepler Conjecture asserts that no arrangement of congruent balls in Euclidean space can have density greater than the familiar pyramid arrangement that is used to stack cannonballs. Sam Ferguson and Thomas Hale gave a computer-assisted proof of this conjecture in 1998, but a large team of referees was unable to certify the correctness of the proof after years of effort. A group of researchers is now developing a formal proof of Kepler's assertion, by formally certifying every algorithm and every last logical inference. This project is approaching completion, and this talk will discuss some of the lessons learned and will describe recent work by Solovyev on formal proofs of nonlinear inequalities.
Thomas C. Hales is the Mellon Professor of Mathematics at the University of Pittsburgh. In 1998, Hales, with the help of his graduate student Samuel Ferguson, proved Kepler's 1611 conjecture (and part of Hilbert's 18th problem) on the most efficient way to stack oranges. Hales's current project, called Flyspeck, seeks to formalize the proof of the Kepler conjecture in the computer proof assistant "HOL Light."
Recorded on Wednesday 21 March 2012.

[@ig2d]

I get that his proof showed that the canon ball arrangement cant be beaten - but was he able to show that it cant even be equalled (ie that it is the only arrangement that achieves maximum packing efficiency...)

[@GolumTR]

The cannonball arrangement (hexagonal close packing) is not the only one, there is also face-centered cubic and other more exotic patterns. This is why the proof is so hard, you can’t exploit the geometry of hexagonal close packing to get the densest arrangement. You have to show any method of packing does at best as well as hexagonal close packing by comparison.