The proof mining seminar is a joint LOS-Institute for Logic and Data Science (ILDS) seminar.
Organizers: Ulrich Kohlenbach, Laurențiu Leuștean and Andrei Sipoș

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.

Wednesday, June 8, 2022

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).

Wednesday, June 29, 2022

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.

Wednesday, July 6, 2022

Pedro Pinto (Technische Universität Darmstadt)

Wednesday, July 13, 2022

Paulo Oliva (Queen Mary University of London)