Right, yes, I should have been clearer, Kolmogorov complexity was just an example of the kind of thing I'm going for. I understand that Kolmogorov complexity do

Right, yes, I should have been clearer, Kolmogorov complexity was just an example of the kind of thing I'm going for. I understand that Kolmogorov complexity doesn't quite cover it, though I don't think this precludes the notion of a measure that /does/ cover the idea of the fundamental complexity of a proof. It sure feels like there's something different about a proof that repeats the same functional form over and over again for 200TB vs 200TB of more complex statements. For example, perhaps there exists somewhere a language that includes the most basic atoms of mathematics, and when you express a proof in that language - like the Principia Mathematica, perhaps - then maybe it's guaranteed to be in irreducable canonical-form, and then you can go on the complexity of that. But I do now see that the 200TB should be considered part of the proof because you haven't verified the proof until you've tried every single item, versus when you've gone through normal short proof you're certain of the result by the end of it.