T. G. Kucera

(Department of Mathematics, University of Manitoba)

Kepler's Conjecture and The Flyspeck Project

Date Friday, October 17, 2014

In 1611 Johannes Kepler, the famous astronomer and mathematician, conjectured (based on earlier work by the English scholar Thomas Harriot) that the usual ''cannonball'' or ''grapefruit'' packing of uniform spheres was the most efficient way of packing spheres in three-space. In modern terms, given any arrangement of non-overlapping spheres of the same radius in three-space, the average volume of the spheres contained within a given radius ( r ) tends to ( frac{pi}{3sqrt{2}}approx 0.740480489ldots) as ( r ) tends to infinity.

The conjecture was finally verified by Thomas Hales in 1998. Or was it? His proof involved not only hundreds of pages of mathematical arguments, but a very large amount of computer calculations. The paper, eventually published in The Annals of Mathematics (2005), was accompanied by a statement from the editors that a large team of mathematicians and their students had only been able to state ''with 99 % certainty'' that the proof was correct and complete.

The Flyspeck Project was a mammoth project led by Hales and sponsored by several large corporations, including MicroSoft, to present a verifiable complete and correct proof of the theorem by computer. The completion of this project was announced this last August (some 10 years or more ahead of initial predictions!).

I will discuss the history of this problem and its solution, and the associated foundational issues, in particular, why we should accept the computer-aided proof if we were dubious about originally published proof.