Is there an $\mathcal{L}$-theory and a formula $\phi$ for which Kolmogorov(proof($\phi$)) $<$ Kolmogorov($\phi$)?
In most "standard" proof systems, the formula $\varphi$ being proved is usually part of the proof itself by definition of the proof system, in which case for all $\varphi$, $K(\varphi) \leq K(\text{proof}) + O(1)$ (the extra constant is for the part of the program which says, basically, "extract the last line of the proof" - anyways, additive $O(1)$ errors are the best one can hope for in Kolmogorov complexity). 

Even in a proof system where all that is required is that the formula $\varphi$ appear somewhere amongst the lines of the proof $\pi$, one can still get $K(\varphi) \leq K(\pi) + O(\log|\pi|)$, where here the extra $\log|\pi|$ bits are used to describe the index $i$ of the line of the proof that corresponds to $\varphi$.

In the much more general Cook-Reckhow style of proof system (or its computable analog) - that is, a polynomial-time computable function $f$ (resp., just a computable function $f$) whose range is exactly the set of true sentences of your theory - again, $K(\varphi) \leq K(\text{proof}) + O(1)$, where here the $O(1)$ extra bits describe the function $f$.

(Note that the trick of hard-coding certain tautologies into your proof system, pointed out by Kaveh, is handled by this latter case, as the hard-coded tautologies must be encoded directly into $f$, so they contribute to/are handled by the $O(1)$.)