Formal Foundations of Discrete Geometry

点击翻译按钮获取中文摘要

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.