For any possible definition of "short", there's only finitely many (and typically few) theorems that have a short proof, while there are infinitely many theorems (not all of them interesting).
More in detail: Proofs are nothing more than strings, and checking the validity of a proof can be done mechanically (and efficiently), so we can just enumerate all valid proofs up to length N and pick out its conclusion.
Where in the article is this discussed?