Proof Mining and Formal Verification

在这个项目中，Avigad建议探索证明理论在三个不同领域的应用：遍历理论和加法组合学中的证明挖掘;数学证明的形式化验证;以及数学的历史和哲学。第一个涉及使用证明理论的方法来提取明确的信息，如收敛速度和界限，从非建设性的数学证明。Avigad将建立在过去的工作，以获得更好的组合和定量信息，从最近的应用遍历理论添加剂组合。第二个涉及使用计算方法，如交互式证明助手，以验证数学证明的正确性。阿维加德已正式验证了素数定理的证明，并为乔治·贡蒂尔（Georges Gonthier）指导的一个雄心勃勃的项目做出了贡献，以验证费特-汤普森定理。在这些经验的基础上，Avigad将开发逻辑基础设施来支持这些努力。最后，Avigad将依靠对数学方法的句法、证明理论的理解来解决数学史和数学哲学中的重要问题。世纪数理逻辑中一些最重要的进步是基于这样一种认识，即数学语言和数学推理规则可以用非常精确的术语来描述。这个项目涉及以三种不同的方式应用这个想法。第一个涉及使用逻辑方法从不同领域的数学证明中分析和提取有用的信息。第二种是使用计算机来验证数学论证和计算的正确性，并辅助数学推理。第三是对数学推理方法有更好的历史和哲学理解。

In this project, Avigad proposes to explore applications of proof theory to three different domains: proof mining in ergodic theory and additive combinatorics; formal verification of mathematical proofs; and the history and philosophy of mathematics. The first involves the use of proof-theoretic methods to extract explicit information, like rates of convergence and bounds, from nonconstructive mathematical proofs. Avigad will build on past work to obtain better combinatorial and quantitative information from recent applications of ergodic theory to additive combinatorics. The second involves using computational methods, such as interactive proof assistants, to verify the correctness of mathematical proofs. Avigad has formally verified a proof of the prime number theorem and has contributed to an ambitious project, directed by Georges Gonthier, to verify the Feit-Thompson theorem. Building on these experiences, Avigad will develop logical infrastructure to support such efforts. Finally, Avigad will rely on a syntactic, proof-theoretic understanding of mathematical methods to address important issues in the history and philosophy of mathematics.Some of the most important advances in mathematical logic in the twentieth century are based on the realization that the language of mathematics and the rules of mathematical reasoning can be described in very precise terms. This project involves applying this idea in three distinct ways. The first involves the use of logical methods to analyze and extract useful information from mathematical proofs in different domains. The second involves the use of computers to verify the correctness of mathematical arguments and calculations, and to assist in mathematical reasoning. The third involves obtaining a better historical and philosophical understanding of the methods of mathematical reasoning.