An invitation to proof mining
The research program of proof mining consists in the extraction of
new information from mathematical proofs, obtained after a logical
analysis using proof-theoretic tools. The new information is both of
quantitative nature (effective bounds), as well as of qualitative
nature (uniformities in the bounds or weakening the premises). This
line of research, developed by Ulrich Kohlenbach in the 1990s, has its
roots in Georg Kreisel's program on unwinding of proofs, put forward
in the 1950s. In this talk we give an introduction to proof mining and
present some recent applications in optimization and nonlinear
analysis.
Laurențiu Leuștean
Last modified: Thu Jan 23 2025