We present preliminary results towards applications of interactive theorem proving to the field of proof mining. Our contribution is twofold. First, we describe an implementation in the Lean proof assistant of the proof-theoretical tools used in the field, which can provide a foundation for a system of program extraction based on general logical metatheorems. Second, we discuss a Lean formalization of quantitative results from convex optimization obtained as part of the program of proof mining.