Ulrich Kohlenbach: Proof Theory : From the Foundations of Mathematics to Applications in Core Mathematics (Workshop CSPM, April 26, 2013 in Toulouse)

In this talk we will give an account of the applied re-orientation of proof theory towards the analysis of concrete proofs in mathematics which was prompted by G. Kreisel's pioneering ideas in the 50's and systematically developed during the last 10-20 years. We will give a survey of uses of proof theoretic transformations in number theory, nonlinear analysis, fixed point theory and ergodic theory. Most recently, even proofs in nonlinear analysis that use a substantial amount of the axiom of choice in the form of Banach limits could be given a quantitative finitary re-interpretation. The success of this program (sometimes called "proof mining") largely vindicates D. Hilbert's original proposal to show that the use of "ideal elements" in the course of proving "real statements" can, in principle, be replaced by an effective finitary reasoning. Surprisingly, this proof-theoretic approach has close connections to the concept of "finitary analysis" as proposed recently by T. Tao.