The Formal Proof of the Kepler Conjecture

开普勒猜想的形式证明

• 批准号: 0804189
• 负责人: Thomas Hales
• 金额: --
• 依托单位: University of Pittsburgh
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-09-15 至 2011-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0804189&HistoricalAwards=false
• 关键词: Formal; Proof; Kepler; Conjecture

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.

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