Collaborative Research: Theoretical Support for Mechanized Proof Assistants

在这个项目中，Avigad和Friedman建议发展数学逻辑的理论基础，以支持数学机械化证明助手的发展。他们建议研究数学的定义结构，并描述定义在实践中使用的方式;研究数论、真实的分析和集合论中初等推理中常用的推理方法，并开发能够反映这些推理形式的算法;并发展了一个丰富的数学证明理论，对数学推理中使用的各种“间接”方法进行了表征和分类。该提案的一个新颖之处在于Avigad和Friedman将关注实际数据，即具体的正式发展。特别是，Avigad将完成素数定理的机械验证证明，并正在开发一个广泛的数论库，使用一个名为Isabelle的证明系统;弗里德曼已经开始在他自己设计的符号框架中使用集合论的完全正式的发展，强调可读性，这项研究的目的是为设计更好的计算机支持的发展，操纵，存储，数学知识的交流。特别是，形式化的密码学和处理它们的方法对于验证硬件和软件系统的行为，例如，以及支持科学计算和密码学都很重要。很好地理解，可用的证明助手的发展将不得不结合联合收割机的纯逻辑推理与务实的工程问题。然而，在今天的专业化学术环境中，相关的社区已经变得很不相交。Avigad和Friedman致力于通过发展强大的理论来弥合差距，这些理论以合理的实践为指导，并旨在支持合理的实践。

In this project, Avigad and Friedman propose to develop a theoretical basein mathematical logic to support the development of mechanized proofassistants for mathematics. They propose to study the definitional structureof mathematics, and characterize the ways that definitions are used inpractice; to study the methods of inference commonly used in elementaryreasoning in number theory, real analysis, and set theory, and to develop ofalgorithms that can mirror these forms of inference; and to develop anenriched theory of mathematical proof to characterize and classify thevarious ``indirect'' methods that are used in mathematical reasoning. Anovel aspect of the proposal is the attention Avigad and Friedman will giveto actual data, i.e. specific formal developments. In particular, Avigadwill complete a mechanically verified proof of the prime number theorem, andis developing a broad number theory library, using a proof system calledIsabelle; and Friedman has begun a fully formal development of set theoryusing in a notational framework of his own devising, with an emphasis onreadability, for a broad audience.This research is intended to contribute to the general goal of devisingbetter computer support for the development, manipulation, storage, andcommunication of mathematical knowledge. In particular, formal mathematicallibraries and means of handling them are important to verify the behavior ofhardware and software systems, for example, and to support scientificcomputing and cryptography. It is well understood that the development ofuseable proof assistants will have to combine pure logical considerationswith pragmatic engineering concerns. However, in today's specializedacademic environments, the relevant communities have become largelydisjoint. Avigad and Friedman are committed to bridging the gap, bydeveloping powerful theory that is guided by, and designed to support, soundpractice.