M1. Applied Proof Theory and the Computational Content of Mathematics

Organisers: Thomas Powell (TU Darmstadt) and Sam Sanders (LMU Munich)

Proof theory is one of the pillars of mathematical logic, and is centered around the idea of treating proofs as mathematical objects which can be formally analysed. While proof theory has its origin in the early 20th century, where it was primarily concerned with foundational problems, modern proof theory is far more focused on applications. In the last few decades the use of sophisticated proof theoretic techniques to extract computational content from proofs has led to important new quantitative results in both mathematics and computer science.

The aim of this symposium is to provide an overview of some exciting recent developments in applied proof theory, and to showcase several new areas in which proof theory is playing a role. The symposium will take place on Thursday 14 September, and will include talks by the following people:

A detailed programme will be published in due course.