The paper On Gödel's theorems on lengths of proofs I: Number of lines and speedup for arithmetics contains quite interesting results on proof length. But some of the details are still, to me, a bit fuzzy [I now find a lot of non-formalized mathematics a bit fuzzy, an occupational hazard it seems].
There is a somewhat related thread on here, but it doesn't link to machine-checked formalizations.
