Proof mining is a paradigm of research, concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of highly infinitary principles. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of a quantitative nature, such as algorithms and effective bounds, as well as of a qualitative nature, such as uniformities in the bounds or weakening the premises. The seminar presents recent results on proof mining.
All seminars, except where otherwise indicated, will be Wednesdays between 16:00 and 17.50. The seminars are online.
To receive announcements about the seminar, please send an email to andrei.sipos@fmi.unibuc.ro.
Ulrich Kohlenbach (Technische Universität Darmstadt)
Recent Applications of Proof Mining in Optimization and Ergodic Theory
Abstract: We will give a brief introduction to proof mining and then discuss
some new devlopments both on the logical side (with N. Pischke)
as well as w.r.t. recent case studies. The latter concern linear
rates of convergence for Tikhonov regularization methods (with
H. Cheval and L. Leustean) and rates of asymptotic regularity and
metastability for nonlinear ergodic theorems in uniformly convex
Banach spaces (with A. Freund).
Nicholas Pischke (Technische Universität Darmstadt)
Proof mining for maximally monotone set-valued operators
Abstract: I discuss how proofs involving set-valued operators and their
resolvents can be treated in higher-type arithmetic while attaining
logical bound extraction theorems. In particular, I focus on a specific
class of so-called ``maximally monotone" operators which are ubiquitous
in the literature. In that context, I discuss how one can circumvent the
logically complicated maximality statement by utilizing Minty's theorem,
a fundamental result from monotone operator theory, and still obtain
mathematically strong systems which allow for the explanation of most of
the previous case studies involving said operators. This leads to a
surprising and robust connection between the maximality statement and
formal extensionality of the operator which I discuss in conjunction
with various quantitative forms of (fragments of) the extensionality
(viz. maximality) statement which can still be used in the context of
the previously mentioned bound extraction theorems.
Pedro Pinto (Technische Universität Darmstadt)
TBA
Paulo Oliva (Queen Mary University of London)
TBA
Horațiu Cheval (LOS)
TBA