The Kepler Conjecture

这个项目将给出离散几何中最古老的问题——开普勒猜想的答案。它断言面心立方填充是可能的密度最大的球体填充之一。现在有一个完善的程序来证明这个猜想。事实上，自20世纪50年代以来，通过L. Fejes Toth的工作，人们已经知道这个问题可以简化为有限数量变量的优化问题。在过去的两年里，计算方法的发展使得开普勒猜想似乎终于触手可及。证明将在很大程度上依赖于计算机计算。线性松弛技术将用一系列线性规划问题代替非线性优化问题。这些线性规划问题往往涉及大约100个变量和不到2000个约束。这种规模的问题通常由计算机解决。为了保证计算机计算的可靠性，将使用IEEE/ANSI机器计算标准，该标准允许在浮点运算中进行定向舍入。这将以区间算术方法为基础，它可以控制计算机计算中出现的舍入误差。在1611年出版的一本小册子中，开普勒描述了已知密度最大的球体排列。他断言，“包装将是尽可能紧密的，因此，在没有其他安排，可以更多的小球被塞进同一个容器。”这一说法后来被称为开普勒猜想。开普勒猜想是离散几何中最古老的问题。这个问题是出了名的难。它有着悠久而辉煌的历史。到目前为止，已经有了一个完善的程序来证明这个猜想。这个项目将完成对开普勒猜想的证明。除了这个猜想的历史重要性之外，球体填充理论已经发展成为各种科学追求中的重要数学工具，例如纠错代码，实验设计和量化问题。这一迅速发展的数学分支的一个最基本的问题将得到解答。该解决方案将使线性规划、全局优化、区间算法和其他基于计算机的技术得到新颖的应用。

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.