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.