That is a long proof, yes, but it doesn't support my point. One could easily imagine a formalization that could compress all that work into a single sentence. W

That is a long proof, yes, but it doesn't support my point. One could easily imagine a formalization that could compress all that work into a single sentence. What you can't do is compress _all_ proofs to single-sentence proofs using a finite number of unique symbols.