Project ID: CNCS-UEFISCDI project number PN-III-P1-1.1-PD-2019-0396, contract no. PD 56/2020.
Host: Simion Stoilow Institute of Mathematics of the Romanian Academy
September 2020 – August 2022
Project description:
Proof mining is an applied subfield of mathematical logic that aims to analyze concrete proofs in mainstream mathematics from the point of view of proof theory. The stated goal of the field is to obtain information which is not immediately apparent, for example computable witnesses and bounds or the superfluousness of some premises. This research paradigm, first suggested by the work of the logician Georg Kreisel in the 1950s and then greatly developed by Ulrich Kohlenbach and his students and collaborators starting in the 1990s, has already been applied to great success in diverse fields such as nonlinear analysis, convex optimization, commutative algebra, ergodic theory or topological dynamics. This project aims to extend this broad research program in multiple ways. First, we shall explore new case studies in nonlinear analysis, approximation theory and optimization in order to find proof arguments where new techniques are needed. Next, we shall consolidate the theoretical basis of the field by developing new metatheorems that may serve as a source or an explanation for the field's concrete results. Lastly, we want to expand the range of applicability of these techniques to areas that are less explored from this perspective like sofic group theory and analytic number theory.
Project research summary:
In the first objective of the project, we have looked at hitherto unanalyzed strong convergence proofs in nonlinear analysis, convex optimization and ergodic theory in order to obtain new effective and uniform rates of metastability, a notion originally introduced by T. Tao and highly sought out in proof mining. In convex optimization specifically, we have further developed our concept of jointly firmly nonexpansive families of mappings, in order to obtain abstract forms of strongly convergent proximal point algorithm, and also we have looked at novel inconsistent feasibility results in the literature in order to extract rates of asymptotic regularity.
For the second objective, which aims to go to the roots of the proof mining, developing new basic tools for it, we have obtained two results. The first one concerns one of the first rates of metastability, namely Tao's own finite convergence principle, which may appear as a Herbrand disjunction of a variable length. We explain logically this result by an appeal to an extension of the Gerhardy/Kohlenbach proof of Herbrand's theorem to first-order arithmetic. The second one, written up in a paper in collaboration with Horațiu Cheval and Laurențiu Leuștean, aims to give a highly abstract form of the fundamental tools of proof mining, the general logical metatheorems, which covers in a uniform and most importantly syntactic way all classes of structures on which proof mining can be done.
In a separate paper, written in collaboration with the project mentor, Liviu Păunescu, we have applied this kind of ideas to the development of a metatheorem for a new class of structures, namely tracial von Neumann algebras. As our investigation can be seen to represent a pilot study in doing proof mining in sofic group theory (with a view towards possible applications in that area), it also connects to the third objective of the project, which focuses on doing proof mining in less-explored areas. In that vein, we have also obtained quantitative results in approximation theory – a conditional strong unicity result for best rational approximation – and in analytic number theory – an elementary proof of a lower bound for $L(1,\chi)$ of order $\sqrt{q}\log q$.
Research team (in alphabetical order):
Scientific reports:
Published papers:
Accepted papers:
Submitted papers:
Organized conferences:
Conference and seminar talks: