Proof mining: a systematic way of analysing proofs

Abstract. We call proof mining the process of logically analyzing proofs in mathe-matics with the aim of obtaining new information. In this survey paper we discuss, by means of examples from mathematics, some of the main techniques used in proof mining. We show that those techniques not only apply to proofs based on classical logic, but also to proofs which involve non-eective principles such as the attainment of the inmum of f 2 C[0, 1] and the convergence for bounded monotone sequences of reals. We also report on recent case studies in approximation theory and xed point theory where new results were obtained. §1. Introduction. Many theorems in mathematics can be expressed as sim-ple equations e.g. stating that x as an element of some Polish space (complete separable metric space) X is a root of a function f: X! R. Theorems of this kind have been called complete. Such (essentially purely universal) theorems do not ask for any eective witnessing information. On the other hand, a theore