The Kepler Conjecture

这个项目将解决开普勒猜想，这是离散几何中最古老的问题。它断言以面为中心的立方体堆积是球体最密集的堆积之一。现在有一个完善的程序来证明这个猜想。事实上，从20世纪50年代S开始，通过托斯的工作，人们就知道这个问题可以归结为有限个变量的最优化问题。在过去的两年里，计算方法已经发展到了开普勒猜想最终似乎可以实现的地步。证据将在很大程度上依赖于计算机计算。利用线性松弛技术将非线性优化问题转化为一系列的线性规划问题。这些线性规划问题往往涉及大约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.