The finitary content of sunny nonexpansive retractions
Andrei 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 …

