The Formal Proof of the Kepler Conjecture

1972年，罗宾·米尔纳在斯坦福大学创建了一个名为LCF（逻辑可计算函数）的证明检查程序。在过去的35年里，一个专门的研究小组一直在不断开发证明检查程序LCF和后续系统。这些程序最终达到了能够检验G. Gonthier的四色定理、PI的Jordan曲线定理、J. Avigad的素数定理等复杂证明的每一个逻辑推理的成熟水平。开普勒猜想断言，三维空间中全等球体的密度永远不会大于/18^1/2，或大约0.74048。这是离散几何中最古老的问题，也是希尔伯特第18个问题的重要组成部分。这个问题一直没有解决近400年，直到1998年弗格森和私家侦探终于破解了它。Flyspeck项目的目的是为开普勒猜想提供一个正式的证明。本课题的研究将完成对Flyspeck项目关键部分的正式论证。这个提议打算遵循G.Gonthier在形式化四色定理时所追求的一般策略，即“将几乎所有数学概念转化为数据结构或程序”。这个提议提供了如何将开普勒猜想证明的已发表文本转换为数据结构或程序的细节。具体地说，许多复杂的证明可以用标记的有根树的集合来表示。该提案的另一部分详细介绍了如何自动证明一系列几何问题。Flyspeck项目已经成为数学和计算机科学领域备受瞩目的项目。在数学、计算机科学和哲学的国际会议上，它已经成为许多受邀演讲的主题。许多研究生（国际）已经参与了这个项目。这种广泛参与将继续下去。《经济学人》（2005）、《科学》（2005）、《自然》（2003）和《纽约时报》等大量发行量广泛的出版物都对PI的Flyspeck提案进行了描述。这个提议有可能重塑数学家处理大规模计算机辅助证明的方式。一般来说，形式化验证方法对于长而复杂的数学证明具有前所未有的可靠性。本提案探索了形式化高度复杂证明的新方法。

In 1972, Robin Milner created a proof-checking program atStanford 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 ofa 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 almostevery mathematical concept into a data structure or a program." This proposalprovides 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 inmath 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 methodsin 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.