Proof Mining and Formal Verification

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

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.