Hmm, I've not been particularly impressed by the massive proofs I've seen recently, e.g. the "Wikipedia-sized proof"[1] that's been doing the rounds. I don't know about this particular proof, but the blowup in size can often come from using a severely limited representation.<p>For example, the "Wikipedia-sized proof" seems to be the variable assignment for a SAT solver, i.e. the problem was reduced to a boolean formula of the form "a AND (b OR c) OR d AND ..." which, because it's such an inexpressive language, requires exponentially more symbols than an equivalent encoding in, say, first-order or higher-order logic. The proof is then an assignment of the form "a = true, b = true, c = false, ..." such that the whole formula evaluates to "true", and this proof is massive precisely because it must encode so many bits.<p>The reason this is a little underwhelming is that mathematicians do not tend to work in terms of boolean satisfiability. Adding just a little expressiveness to the language can make statements and proofs much shorter, and mathematicians tend to work at very high levels of abstraction.<p>Another reason why such proofs are underwhelming is that they don't really give us any insights which we could re-use to perform other proofs; we'd just have to start the solver from scratch on the new problem.<p>All they really tell us is that a proof exists, and hence the statement is true rather than false. So, in effect, these "huge" proofs only really contain a single bit of information. This can be made rigorous using algorithmic information theory: given some encoding of the problem (allowed axioms and deduction rules, plus the theorem statement) we only need a constant number of bits to make a proof-searching program which enumerates all allowed rules applied to all allowed axioms in all allowed ways, and halts when one satisfies the theorem statement. The only unknown is whether the program will halt, and that's the bit given by the proof. All of the rest of the proof is redundant, since it can be generated (i.e. decompressed) by running the program, since we know that it halts.<p>Anything else is basically a time/space tradeoff, to avoid having to wait for such an enumerating program to finish. I'm pretty sure such gigantic proofs are not pareto-optimal though (i.e. there's probably another proof out there which is both shorter and faster to "decompress").<p>Of course, there's also the point that it's trivial to construct theorems which require ridiculously long proofs (in some particular representation, no matter how powerful) [2].<p>[1] <a href="https://www.newscientist.com/article/dn25068-wikipedia-size-maths-proof-too-big-for-humans-to-check/" rel="nofollow">https://www.newscientist.com/article/dn25068-wikipedia-size-...</a><p>[2] <a href="https://en.wikipedia.org/wiki/G%C3%B6del%27s_speed-up_theorem" rel="nofollow">https://en.wikipedia.org/wiki/G%C3%B6del%27s_speed-up_theore...</a>