 Gödel’s 1936 ‘Speed-up’ theorem, published in an abstract “On the length of proofs”, Gödel 1936 says that while some sentences of arithmetic are true but unprovable, there are other sentences which are provable, but even the shortest proof is longer than any bound given in advance as a recursive function of the sentence. More exactly: