Formal Foundations of Discrete Geometry

摘要奖：DMS-0503447首席研究员：Thomas C.Hales1972年，Robin Milner创建了一个校对程序LCF(用于“可计算函数的逻辑”)。自那时以来，校对程序LCF及其后代一直在不断发展。这些程序终于达到了成熟的程度，它们能够检查极其复杂的数学证明的每一个逻辑推理。随着计算机辅助几何证明的数量明显增加，计算机代码可能不会像传统证明那样受到同样仔细的审查。一种解决方案是让数学家显著增加他们对形式方法的使用，特别是当证明是计算机辅助的时候。这一建议的目的是在一个这样的系统中建立离散几何的基础(HOL-LIGHT是高级逻辑的缩写，是LCF的后代之一)。离散几何的基础将发展到正式建立几个经典定理的阶段。要形式化的定理包括罗杰斯在球包装中的界，以及13个球的问题(牛顿-格雷戈里问题)。传统的数学证明是以一种便于数学家理解的方式写成的。省略了常规的逻辑步骤。在传统的校对中，大量的上下文是由读者承担的。证明，特别是在几何及相关领域中，依赖于受过训练的数学家能够将这些直观的论证转化为更严格的论证的情况下的直觉论证。相比之下，在形式证明中，提供了所有中间的逻辑步骤。即使从直觉到逻辑的转换是例行公事，也不会诉诸直觉。因此，形式证明不那么直观，也不太容易受到逻辑警报的影响。在过去，形式证明对于任何显著复杂的数学论证都不是一种实用的可能性。然而，过去30年的技术进步使极其复杂的数学证明有可能扩展为正式的证明。计算机被用来检查是否提供了每一个逻辑步骤。这个项目将从形式上从离散几何(特别是球体填充的主题)建立基础材料。这是几何分析和基础程序的联合奖项。

AbstractAward: DMS-0503447Principal Investigator: Thomas C. HalesIn 1972, Robin Milner created a proof-checking program LCF (for"Logic for Computable Functions"). The proof-checking programLCF and its descendants have been in continual development sincethen. These programs have finally reached the level of maturitythat they are capable of checking every logical inference ofextremely complex mathematical proofs.With a noticeable increase in the number of computer-assistedproofs in geometry there are dangers that computer code will notbe scrutinized with the same care as traditional proofs. Onesolution is for mathematicians to significantly increase theiruse of formal methods, particularly when proofs are computerassisted. The purpose of this proposal is to build thefoundations of discrete geometry within one such system(HOL-light, short for Higher Order Logic, is one of thedescendants of LCF).The foundations of discrete geometry will be developed to thestage where several classical theorems will be formallyestablished. The theorems to be formalized include Rogers'sbound in sphere packings, and the problem of 13 spheres (theNewton-Gregory problem).Traditional mathematical proofs are written in a way to make themeasily understood by mathematicians. Routine logical steps areomitted. In a traditional proof, an enormous amount of context isassumed on the part of the reader. Proofs, especially in geometryand related areas, rely on intuitive arguments in situationswhere a trained mathematician would be capable of translatingthose intuitive arguments into a more rigorous argument.By contrast, in a formal proof, all the intermediate logicalsteps are supplied. No appeal is made to intuition, even if thetranslation from intuition to logic is routine. Thus, a formalproof is less intuitive, and yet less susceptible to logicalerrors.In the past, formal proofs were not a practical possibility formathematical arguments of any significant complexity. However,technological advances over the past 30 years have made itpossible for extremely complex mathematical proofs to be expandedinto a formal proof. Computers are used to check that everylogical step has been supplied.This project will establish foundational material from discretegeometry (especially the topic of sphere packings) from a formalstandpoint.This is a joint award of the programs in Geometric Analysis and Foundations.