Deep theorems and long proofs I ran across this discussion by Daniel Shanks,

"Is the quadratic reciprocity law a deep theorem?."
  Solved and Unsolved Problems in Number Theory. Vol. 297. AMS, 2001. p.64ff.

which made me wonder:

Q. Is there a theorem in some formal system whose proofs are known to be
  necessarily "long" in some sense, perhaps in the Kolmogorov-complexity sense?

I know it has been established that there are relatively "short" theorems that have
only enormously "long" proofs (apparently[?] due to Gödel,"On the length of proofs"),
but I'm asking if it is known that some
particular theorem only has long proofs?
(This is in some sense the obverse of the MO compendium,
"Quick proofs of hard theorems.")
Obviously this is a naive question!
 A: If you're willing to accept a contrived statement, then it's not hard to get an explicit example, but this may not be the sort of example you're looking for.
Following Gödel's approach, you can make a statement of the form "I have no formal proof of less than a hundred pages."  (More precisely, you should use implicit self reference, along the lines of "There is no formal proof of less than a hundred pages for this string followed by its quotation: 'There is no formal proof of less than a hundred pages for this string followed by its quotation:'")
Assuming your formal system is consistent, this statement cannot be proved in less than a hundred pages.  In that case it actually is provable, because you can prove it by enumerating all possible proofs of less than a hundred pages and checking that they don't work.  Thus, we have a relatively short theorem that has no short formal proof.  Sadly, the theorem is of no intrinsic interest.
Note that the reason it didn't take us a hundred pages to prove the theorem is because we assumed the formal system was consistent.  By Gödel's second incompleteness theorem, the system can't prove its own consistency, so this approach is not available within the system.  In fact, this argument proves the second incompleteness theorem: if consistency had a short enough proof, then we could carry out this argument to prove the theorem in under a hundred pages.  There's nothing special about a hundred pages in this argument, so there can be no proof of consistency at all.  This approach to the second incompleteness theorem is fundamentally the same as Gödel's original proof.
Here I've been measuring proofs by length, rather than the Kolmogorov complexity mentioned in the question.  That's not a useful measure for proofs, because you can reconstruct the shortest proof of theorem X in system S from little more than X and a proof checker for S (which you apply to do a brute force search for the shortest proof).  This means if you fix S, the Kolmogorov complexity of the shortest proof is no more than an additive constant greater than that of the theorem itself.
A: There is a body of very interesting work surrounding the proof complexity of various formulations of the well-known pigeon-hole principle, the fact that there is no injective function from a set of size $m$ to a set of size $n$, when $m\gt n$. It turns out that the difficulty of proving this depends on how much bigger $m$ is than $n$, and so we have actually a variety of pigeon-hole principles here:


*

*Pigeon-hole principle. There is no injective map $n+1\to n$ for natural numbers $n$.

*Moderately weak pigeon-hole principle. There is no injection $2n\to n$, for positive natural numbers $n$. 

*Weak pigeon-hole principle. There is no injection from $n^2\to n$ for natural numbers $n>1$. 

*Very weak pigeon-hold principle. There is no injection $\infty\to n$, for any finite $n$. 
The principles become easier to prove, of course, as the domain gets larger, and there are shorter proofs when the domain is very large. The paper Proof complexity of pigeon-hole principles by Alexander Rozborov contains many interesting results on the computational proof complexity of these various formulations of the pigeon-hole principle, and in particular of the necessary long lengths of proofs in certain systems. Meanwhile, results of Sam Buss, Polynomial size proofs of the propositional pigeon-hole principle show that there is a dependence on the particular proof system that is adopted, for in certain Frege system one can still obtain polynomial size proofs. 
