Collaborative Research: Theoretical Support for Mechanized Proof Assistants

在这个项目中，阿维加德和弗里德曼建议建立一个数理逻辑的理论基础，以支持数学机械化校对助理的发展。他们建议研究数学的定义结构，并描述定义在实践中的使用方式；研究数论、实分析和集合论中基本推理中常用的推理方法，并开发能够反映这些推理形式的算法；以及发展丰富的数学证明理论，以表征和分类数学推理中使用的各种“间接”方法。该提案的另一个方面是阿维加德和弗里德曼将关注实际数据，即具体的正式发展。特别是，阿维加德将完成素数定理的机械验证证明，并正在开发一个广泛的数论库，使用一个名为Isabelle的证明系统；弗里德曼已经开始在他自己设计的符号框架内为广大读者使用集合论的完全正式的发展。这项研究旨在为数学知识的发展、操作、存储和交流设计更好的计算机支持这一总体目标。特别是，正式的数学库和处理它们的方法对于验证硬件和软件系统的行为以及支持科学计算和密码学是重要的。众所周知，开发可用的证明助手必须将纯粹的逻辑考虑与实际的工程考虑结合起来。然而，在当今专业化的学术环境中，相关社区已经变得基本上脱节。阿维加德和弗里德曼致力于通过发展强大的理论来弥合这一差距，这些理论以健全的实践为指导，并旨在支持这些实践。

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.