This project will give a solution to the Kepler conjecture, the oldest problem in discrete geometry. It asserts that the face-centered cubic packing is one of the densest possible packing of spheres. There is now a well-developed program for proving the conjecture. In fact, it has been known since the 1950's, through the work of L. Fejes Toth, that this problem can be reduced to an optimization problem in a finite number of variables. Over the last two years, the computational methods have been developed to the point that the Kepler conjecture finally appears to be within reach. The proof will rely heavily on computer calculations. Linear relaxation techniques will be used to replace the nonlinear optimization problem with a series of linear programming problems. These linear programming problems tend to involve about a hundred variables and less than two thousand constraints. Problems of this size are routinely solved by computer. To guarantee the reliability of computer calculations, IEEE/ANSI standards of machine computation, which permit directed rounding in floating-point arithmetic, will be used. This will be based on methods of interval arithmetic, which give control over the round-off errors that arise in computer calculations. In a booklet published in 1611, Kepler described the densest known arrangement of spheres. He asserted that "the packing will be the tightest possible, so that in no other arrangement could more pellets be stuffed into the same container." This claim has come to be known as the Kepler conjecture. The Kepler conjecture is the oldest problem in discrete geometry. The problem is notoriously difficult. It has a long and distinguished history. By now, there is a well-developed program for proving the conjecture. This project will complete a proof of the Kepler conjecture. In addition to the historical importance of the conjecture, the theory of sphere packings has developed as an important mathematical tool in various scientific pursuits, such as error-correc ting codes, experimental design, and quantization problems. One of the most fundamental questions of this rapidly growing branch of mathematics will be answered. The solution will make a novel application of linear programming, global optimization, interval arithmetic, and other computer-based technologieq.
