For example, the statement: is provable in Peano arithmetic (PA) but the shortest proof has at least a googolplex symbols, by an argument similar to the proof of Gödel's first incompleteness theorem: If PA is consistent, then it cannot prove the statement in fewer than a googolplex symbols, because the existence of such a proof would itself be a theorem of PA, a contradiction.
Harvey Friedman found some explicit natural examples of this phenomenon, giving some explicit statements in Peano arithmetic and other formal systems whose shortest proofs are ridiculously long (Smoryński 1982).
For example, the statement is provable in Peano arithmetic, but the shortest proof has length at least A(1000), where A(0) = 1 and A(n+1) = 2A(n).
The statement is a special case of Kruskal's theorem and has a short proof in second order arithmetic.
If one takes Peano arithmetic together with the negation of the statement above, one obtains an inconsistent theory whose shortest known contradiction is equivalently long.