Proof Mining: from proof-theoretic foundations to applications in core mathematics

  • Date September 18, 2018
  • Hour 3 pm
  • Room GSSI Library
  • Speaker Ulrich Kohlenbach (Technische Universität Darmstadt, Germany)
  • Area Computer Science


During the last two decades a systematic program of "proof mining" has emerged as a new applied form of proof theory and has successfully been used in a number of areas of core mathematics. Here one interprets given, prima facie noneffective, proofs in terms of suitable functional programs which exhibit the hidden computational content of the proof. The main tools used are novel forms and extensions of Kurt Goedel's famous functional ("Dialectica") interpretation (published in his last paper in 1958). We will discuss some specific applications in the context of nonlinear analysis (convex optimization, ergodic theory and abstract Cauchy problems) resulting e.g. in new explicit rates of convergence.

Biographical sketch: Since 2004. Ulrich Kohlenbach is full professor and Chair for Algebra and Logic at the Department of Mathematics of the Technische Universität Darmstadt. He has also held academic positions at the Department of Computer Science, University of Aarhus, Denmark, the Department of Mathematics, University of Michigan, Ann Arbor, and the Department of Mathematics at the University of Frankfurt. He has been the PI of the Darmstadt-Toyko PhD school on Mathematical Fluid Dynamics. He was an invited speaker (section Logic and Foundations) at ICM 2018 in Rio;recipient of a Kurt Gödel Research Prize Fellowship 2011 (category: unrestricted) of the Kurt Gödel Society (a personal prize of 100,000 EUR and a gold medal). His research focuses on logic (in particular proof theory, computability theory and constructive reasoning) with applications to mathematics and computer science, computational content of proofs, proof interpretations and their use in mathematics, functionals of higher type, approximation theory, nonlinear analysis, fixed point theory, ergodic theory, abstract Cauchy problems, and convex feasibility problems.