The finitary content of sunny nonexpansive retractions
Facultatea de Matematica si Informatica, sala 202Andrei Sipoș (TU Darmstadt & IMAR). The goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often, such proofs make use of strong mathematical principles, but a preliminary analysis may show that they are not actually needed, so the proof may be carried …