Proofs in mathematical practice serve to warrant the truth of mathematical theorems. Proof theory, i.e. the abstract study of proofs in logic, arose from Hilbert’s programme for the foundations of mathematics; the aim of the latter was to put abstract mathematics on a firm formal basis by proving its consistency in the meta-mathematics and by finitary methods only. Gödel's incompleteness theorems allegedly show the impossibility of Hilbert's programme as such but thus have stood and mark the beginning of a seminal paradigm shift in proof theory: to use mathematical proofs as a rich source of computational information such as certfied algorithms and effective bounds. Current research in this fast-growing area is known under terms such as dynamical methods, program extraction, and proof mining in mathematics, computer science, and philosophy. Our aim is to present all aspects of the state-of-the-art and foster interdisciplinary exchange