Proof theory has its origin in what has been called ‘Hilbert’s program’: Since the 19th century noneffective and nonfinitary (set-theoretic) principles became increasingly important which raised the issue of their legitimacy. Hilbert’s approach was to establish the consistency of a suitable formalization T of mathematics (first number theory and then analysis and set theory) within some finitary reasoning FIN. This would then imply that any purely universal number theoretic (‘real’) statement which is provable in T would already be provable in FIN. So nonconstructive (‘ideal’) elements in proofs of real statements could in principle be eliminated. Hilbert already and then later, in particular, Kreisel considered the broader goal to achieve this for more general statements such as ∀∃-statements φ in number theory (i.e. Π^0_2-statements). In fact, the proof-theoretic tools developed in the course of the consistency program by Hilbert and his school extract - as was hightlighted first by Kreisel - explicit algorithms p witnessing the existential quantifier in φ from a proof of φ in - say - Peano arithmetic PA. Whereas often Hilbert’s concept of finitary reasoning FIM
is identified with primitive recursive arithmetic PRA, Hilbert himself saw in 1925 that an extension of PRA to the primitive recursive functionals of finite types (nowadays called Godel’s T) is necessary already for number theory and in 1941 Godel showed by means of his functional interpretation that any proof of a theorem (of any complexity) in Peano arithmetic PA allows for a suitable algorithmic reading in terms of T.

In this talk we view Hilbert’s program in this applied form due to Kreisel as the program to eliminate ideal elements from proofs of computationally meaningful statements with the goal of extracting explicit numerical information such as bounds etc. In fact, already in the larger Hilbert school, this was approached e.g. in the context of abstract algebra in Grete Hermann’s dissertation (written under the supervision of Emmy Noether).
Since 1990, the author has launched the program of ‘proof mining’ which aims to achieve this for large parts of (mainly nonlinear) analysis such as fixed point theory, ergodic theory, abstract Cauchy problems and nonsmooth optimization. In more than 100 case studies carried out by many authors it has turned out that even proofs which prima facie use highly nonconstructive tools allow for the extraction of explicit effective bounds which not only are (in all cases so far) definable in Godel’s
T but usually even of very low complexity going down in important situations to polynomial and - most recently - even linear bounds. We will discuss this ‘proof-theoretic tameness’ of large parts of ordinary mathematics and provide a couple of examples which show the general spirit of proof mining as an applied form of Hilbert’s program.