Formal Foundations of Discrete Geometry

摘要：奖：dms -0503447首席研究员：Thomas C. hales1972年，Robin Milner创建了一个证明检查程序LCF（“Logic for Computable Functions”）。从那时起，证明检查程序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.