While I think what your saying is true, it's frowned upon. It's saying "I've discovered a truly marvelous proof and its at the bottom of this cave". We've dodged the infinity risk, but not the resources involved in communication risk.

So it's kind of just crap UI at this point. I think that given that proofs are essentially social objects, this is a pretty big negative on that style of proof even if it doesn't totally sink the ship.

The communication is easy. You show someone your nice compact program, and they don't have to run it to understand it.

A 200TB proof is literally impossible to communicate to a human. Where is the benefit to that formulation?

The huge version is not better for a machine either. 200TB is a lot of storage, and you could rerun 30000 CPU-hours of calculations in under a month on a single semi-high-end 4U server.

But if I don't trust you then your program and limit can only be verified by my execution of it. This might be incredibly or even in feasibly expensive and unless you've also got a resource bound proof then I might be sunk.

On the other hand, code which verified a fully expanded proof may be very simple and easy to check/trust/believe.