i would imagine a proof has several "uses": 1) the proof itself is useful for some other result or proof, and 2), the proof is using a novel technique or uses n

i would imagine a proof has several "uses": 1) the proof itself is useful for some other result or proof, and 2), the proof is using a novel technique or uses novel maths, or links to previously unlinked fields, and it's not the proof's result itself that is useful, but the technique developed. This technique can then be applied in other areas to produce other kinds of proofs or knowledge. I suspect it is the latter that will suffer in automated proofs perhaps - without understanding the techniques, or if the technique is not really novel but just tedious.