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.
