Principal Investigator: Thomas C. Hales
In 1972, Robin Milner created a proof-checking program LCF (for "Logic for Computable Functions"). The proof-checking program LCF and its descendants have been in continual development since then. These programs have finally reached the level of maturity that they are capable of checking every logical inference of extremely complex mathematical proofs.
With a noticeable increase in the number of computer-assisted proofs in geometry there are dangers that computer code will not be scrutinized with the same care as traditional proofs. One solution is for mathematicians to significantly increase their use of formal methods, particularly when proofs are computer assisted. The purpose of this proposal is to build the foundations of discrete geometry within one such system (HOL-light, short for Higher Order Logic, is one of the descendants of LCF).
The foundations of discrete geometry will be developed to the stage where several classical theorems will be formally established. The theorems to be formalized include Rogers's bound in sphere packings, and the problem of 13 spheres (the Newton-Gregory problem).
Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. In a traditional proof, an enormous amount of context is assumed on the part of the reader. Proofs, especially in geometry and related areas, rely on intuitive arguments in situations where a trained mathematician would be capable of translating those intuitive arguments into a more rigorous argument.
By contrast, in a formal proof, all the intermediate logical steps are supplied. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors.
In the past, formal proofs were not a practical possibility for mathematical arguments of any significant complexity. However, technological advances over the past 30 years have made it possible for extremely complex mathematical proofs to be expanded into a formal proof. Computers are used to check that every logical step has been supplied.
This project will establish foundational material from discrete geometry (especially the topic of sphere packings) from a formal standpoint.
This is a joint award of the programs in Geometric Analysis and Foundations.
