>A 200TB proof is already incomprehensible to humans.

Not really, since what matters is the compressibility of the proof, not its size.

We might not be able to read all individual clauses, but it's enough that we know how the clauses are constructed.