Gödel's speed-up theorem
In mathematics, Gödel's speed-up theorem, proved by Gödel (1936), shows that there are theorems whose proofs can be drastically shortened by working in more powerful axiomatic systems. 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 unimaginably long.