Laurenţiu Leuştean
University of Bucharest and Simion Stoilow Institute of Mathematics of the Romanian Academy

The research program of proof mining is concerned with the extraction of hidden finitary content from mathematical proofs. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of quantitative nature, such as algorithms and effective bounds, as well as of qualitative nature, such as uniformities in the bounds or weakening the premises. Thus, even if one is not particularly interested in the numerical details of the bounds themselves, in many cases such explicit bounds immediately show the independence of the quantity in question from certain input data. This line of research, developed by Kohlenbach in the 1990's, has its roots in Kreisel's program on unwinding of proofs, put forward in the 1950's. In this talk we give an introduction to proof mining and present some recent applications in optimization and nonlinear analysis.