Proof Theory: Finite Data from Infinite Mathematics

许多数学问题可以用多种方法解决，每种方法都有自己的优点。 简短的概念性证明可以避免复杂的计算，但有时无法提供计算所揭示的详细定量信息。 最近的一个见解是，有时候，数学可以有两种方式。 通过研究数学证明本身的结构，来自被称为证明理论的领域的技术使抽象证明和从中提取详细计算成为可能。 相反，这些技术可以采用某些冗长的计算，并将其替换为简短、抽象的论点，然后将其推广以证明新的结果。 该项目的重点是进一步将这些技术扩展到新的领域，特别是最近发现的统计应用，以及继续将已知技术应用于新的问题，特别是在概率和随机性发挥核心作用的领域。在这个项目中，Towsner将建立在以前的应用超积研究数学对象可以分为结构化和随机部分的方式。 一个明确的定量方法，这样的二分法一直是中央极值图论，但最近的工作表明，这些也可以被视为在测量理论方面，通过使用超产品调解之间的有限和无限的观点，导致新的结果在该地区。 Towsner将系统地研究这种联系，既在无限环境中开发新的工具，又使用证明论的功能解释将这些工具翻译回经典环境，从这些无限参数中提取明确的计算。

Many mathematical questions can be solved in multiple ways, each with its own advantages. Short, conceptual proofs can avoid complicated calculations, but sometimes cannot provide the detailed quantitative information those calculations would reveal. A recent insight is that, sometimes, mathematics can have it both ways. By studying the structure of mathematical proof itself, techniques from the field known as proof theory make it possible to take abstract proofs and to extract detailed calculations from them. Used in the opposite direction, these techniques can take certain kinds of lengthy calculations and replace them with short, abstract arguments which can then be generalized to prove new results. The focus of this project is to both further extend these techniques to new areas, particularly recently discovered applications in statistics, as well as continue the application of known techniques to new problems, especially in areas where probability and randomness play a central role.In this project, Towsner will build on previous applications of ultraproducts to studying the way mathematical objects can be separated into structured and random parts. An explicit quantitative approach to such dichotomies has long been central to extremal graph theory, but recent work has shown that these can also be viewed in measure-theoretic terms by using ultraproducts to mediate between the finitary and infinitary perspectives, leading to new results in the area. Towsner will study this connection systematically, both developing new tools in the infinitary setting and using the proof-theoretic functional interpretation to translate these tools back to the classical setting, extracting explicit calculations from these infinitary arguments.