The Formal Proof of the Kepler Conjecture

University Of Pittsburgh, Pittsburgh PA

Investigators

Abstract

In 1972, Robin Milner created a proof-checking program at Stanford University called LCF (Logic for Computable Functions). The proof-checking program LCF and subsequent systems have been under continual development by a dedicated group of researchers over the past 35 years. These programs have finally reached the level of maturity that they are capable of checking every logical inference of complex proofs such as the Four-color theorem by G. Gonthier, the Jordan curve theorem by the PI, and the Prime number theorem by J. Avigad. The Kepler Conjecture asserts that the density of a packing of congruent spheres in three dimensions is never greater than pi/18^1/2, or approximately 0.74048. This is the oldest problem in discrete geometry and is an important part of Hilbert's 18th problem. The problem remained unsolved for nearly 400 years until it was finally cracked in 1998 by S. Ferguson and the PI. The purpose of the Flyspeck project is to produce a formal proof of the Kepler conjecture. The research of this proposal will complete the formal proof of the key parts of the Flyspeck Project. This proposal intends to follow the same general strategy that was pursued by G. Gonthier in the formalization of the Four-Color theorem, that is, "to turn almost every mathematical concept into a data structure or a program." This proposal provides detail about how the published text of the proof of the Kepler conjecture is to be converted to data structures or program. Specifically, many intricate proofs can be represented in terms of a collection of labeled rooted trees. Another part of the proposal gives details about how to automate the proofs of a collection of problems in geometry. The Flyspeck project has become a high-profile project in math and computer science. It has already been the subject of many invited presentations at international conferences in math, computer science, and philosophy. A number of graduate students (internationally) have become involved in the project. This broad participation will continue. The PI's Flyspeck proposal has been described in a large number of publications with wide circulation, including the Economist (2005), Science (2005), Nature (2003), and the New York Times. This proposal has the potential to reshape the way mathematicians approach large-scale computer-assisted proofs. Formal verification methods in general have the potential to unprecedented levels of reliability to long and complex mathematical proofs. This proposal explores novel methods to formalize a highly complex proof.