It is the second thing. Anyway, the number of pages is arbitrary -- it is a function of your language and terminology. Not every proof can be simplified, so surely there exist useful proofs that require 10,000 pages minimum for a given finite set of terms.
So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.
> surely there exist useful proofs that require 10,000 pages minimum
The classification of finite simple groups "consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."[1]
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.
So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.