constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
The Chaitin incompleteness theorem is a kind of incompleteness theorem in the context of complexity theory. It says roughly that within any sufficiently strong formal system $S$, there is an upper bound on provable complexity: a natural number $L$ such that for no given string of data is there is a formal proof in $S$ that its Kolmogorov complexity exceeds $L$.
Note that $L$ is not an upper bound on complexity; on the contrary, there are only finitely many strings with complexity $L$ or less, and all of the infinitely many others must have complexity larger than $L$. The system $S$ may even be capable of proving this, but it still cannot prove any particular example.
Gregory Chaitin, Algorithmic Information Theory, 2003. (first edition 1987) (pdf)
Gregory Chaitin, The Limits of Mathematics, 1994 (arXiv:chao-dyn/9407003)
Expositions and surveys include
Wikipedia, Chaitinâ€™s incompleteness theorem
John Baez, Surprises in logic, 2011