There are several proofs that would be far longer than this if the details of the computer calculations they depend on were published in full.
Some typical examples of such theorems include: Kurt Gödel showed how to find explicit examples of statements in formal systems that are provable in that system but whose shortest proof is absurdly long.
For example, the statement: is provable in Peano arithmetic but the shortest proof has at least a googolplex symbols.
For example, the statement is provable in Peano arithmetic, but the shortest proof has length at least 10002, where 02 = 1 and n + 12 = 2(n2) (tetrational growth).
The statement is a special case of Kruskal's theorem and has a short proof in second order arithmetic.