Horatiu Cheval
University of Bucharest, Bucharest, Romania

Proof mining is a research program in applied logic developed by Ulrich Kohlenbach and his collaborators since the 1990’s, concerned with the extraction of hidden effective results from nonconstructive mathematical proofs, through an analysis guided by proof theoretical tools. In this talk, we will present some recent results in optimization and nonlinear analysis obtained in the context of proof mining. We will also discuss the potential applications of interactive theorem proving to the field, and implementations in the Lean proof assistant of some results and techniques from proof mining.