Collaborative Research: Theoretical Support for Mechanized Proof Assistants

Ohio State University Research Foundation -Do Not Use, Columbus OH

Investigators

Abstract

In this project, Avigad and Friedman propose to develop a theoretical base in mathematical logic to support the development of mechanized proof assistants for mathematics. They propose to study the definitional structure of mathematics, and characterize the ways that definitions are used in practice; to study the methods of inference commonly used in elementary reasoning in number theory, real analysis, and set theory, and to develop of algorithms that can mirror these forms of inference; and to develop an enriched theory of mathematical proof to characterize and classify the various ``indirect'' methods that are used in mathematical reasoning. A novel aspect of the proposal is the attention Avigad and Friedman will give to actual data, i.e. specific formal developments. In particular, Avigad will complete a mechanically verified proof of the prime number theorem, and is developing a broad number theory library, using a proof system called Isabelle; and Friedman has begun a fully formal development of set theory using in a notational framework of his own devising, with an emphasis on readability, for a broad audience. This research is intended to contribute to the general goal of devising better computer support for the development, manipulation, storage, and communication of mathematical knowledge. In particular, formal mathematical libraries and means of handling them are important to verify the behavior of hardware and software systems, for example, and to support scientific computing and cryptography. It is well understood that the development of useable proof assistants will have to combine pure logical considerations with pragmatic engineering concerns. However, in today's specialized academic environments, the relevant communities have become largely disjoint. Avigad and Friedman are committed to bridging the gap, by developing powerful theory that is guided by, and designed to support, sound practice.