collaborative research: theoretical support for mechanized proof assistants

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

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.