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.