In this talk we give a survey on recent applications of the âproof miningâ program. This program is concerned with the extraction effective uniform bounds from ineffective proofs in analysis using techniques from proof theory. We will focus on problems in ergodic theory. More specifically, we discuss new explicit uniform rates of metastability (in the sense of Tao) for the von Neumann Mean Ergodic Theorem (for uniformly convex Banach spaces) as well as several nonlinear ergodic theorems (in the Hilbert space case) due to Baillon and Wittmann.