Prof. Thomas Callister Hales gave a lecture titled “the Formal Proof of the Kepler Conjecture” at AMSS on 22, July, 2015.

In his talk, Kepler asserted that no packing of congruent balls in space can have density greater than the familiar cannonball arrangement in 1611. This statement, known as the Kepler conjecture, is now a theorem that has been formally verified. A theorem is formally verified if every step of the proof has been checked at the level of the primitive inference rules of logic and the foundational axioms of mathematics. This talk presented the Kepler conjecture, its proof, and background about the formal verification of theorems.      

Prof. Thomas Callister Hales is an American mathematician working on the Langlands program. He is known in the area for having worked on the fundamental lemma, and proving a special case of it over the group. Many of his ideas were incorporated into the final proof, due to Ngô Bảo Châu. He is also known for his 1998 computer-aided proof of the Kepler conjecture, a centuries-old problem in discrete geometry which states that the most space-efficient way to pack spheres is in a pyramid shape. Hales also proved the honeycomb conjecture.