Proof mining is a research paradigm which aims to analyze concrete proofs in mainstream mathematics using tools from mathematical logic – specifically proof theory – in order to reveal information which may not be immediately apparent. This information may be qualitative, like the elimination of superfluous premises, quantitative, like the determination of explicit witnesses or bounds for existentially quantified variables, or mixed, like the uniformity of the latter quantities with respect to parameters of the problem.
The idea originated with Georg Kreisel in the 1950s and was given much of its current form by the school of Ulrich Kohlenbach, starting in the 1990s. Currently, there are working groups of proof mining at universities and research institutes in several locations, including Bath, Bucharest, Darmstadt and Lisbon.
Foto: © Thomas Ott / TU Darmstadt