Proof Mining: Foundations and Applications
Ulrich Kohlenbach (TU Darmstadt)
Proof Mining is an applied form of proof theory which utilizes proof-theoretic transformations to extract new computational information (e.g. programs or effective bounds) as well as qualitative generalizations from given prima facie noneffective proofs in different areas of core mathematics. This logic-based methodology applies so-called proof interpretations which are modern extensions and adaptions of Goedel's famous functional ('Dialectica') interpretation as well as embeddings of classical reasoning into approximately constructive (`intuitionistic') reasoning. Combined with a regime to control bounding data throughout higher types by logical relations (`majorization') this can be made into a powerful tool in the form of logical metatheorems to extract effective and highly uniform bounds from proofs which make use even of strong noneffective principles. This methodology has been applied during the past 25 years with particular success in areas of nonlinear analysis such as fixed point theory, ergodic theory and - in recent years - to nonsmooth optimization.
We will discuss the proof-theoretic background behind this development and survey a few recent applications to topics in optimization which are also relevant in connection with machine learning.