Comment by Koshkin

Sure, "proof mining" is feasible, but the goal of proving a theorem is only rarely finding any proof, it is rather finding a proof that makes sense, is "elegant", and in the best case scenario a proof that actually forms a sensible new theoretical framework in which the theorem becomes almost trivial to prove.