An exploration of proof mining I
Andrei Sipoș
Chair: Paul-André Melliès
Proof mining is a research paradigm connected to mathematical logic that aims to analyze concrete proofs in mainstream mathematics using tools originating in proof theory in order to reveal information which is not immediately apparent. This information may be qualitative, like eliminating premises, quantitative, like the determination of witnesses and bounds for existentially quantified variables, or mixed, like the uniformity of the latter quantities with respect to parameters of the problem. The paradigm originated with Georg Kreisel in the 1950s and reached its current mature form within the school of Ulrich Kohlenbach.
I aim to briefly present the theoretical underpinnings of proof mining but largely adopt a hands-on approach via focusing on a plethora of increasingly complex case studies, of which I mention Ulrich Berger’s didactic example for the classical Herbrand theorem, Terence Tao’s finite monotone convergence principle, my own analysis of a convergence theorem on the unit interval due to D. Borwein and J. Borwein, and the finitary content of sunny nonexpansive retractions (joint work with U. Kohlenbach).