Maybe we could define the Kolmogorov complexity of a proof as the number of lines of code, PLUS the size of the proof that the proof-generating program halts.

Or the total number of lines of code in a sequence of programs, where the first program generates a proof of the original theorem, and every other program generates a proof that the preceding program halts, PLUS the size of a proof that the final program halts.