 The Speed-up Theorem is the result of contemplating and elaborating the proof of the incompleteness theorem. It applies the fixed-point technique to the concept of unprovability by a short proof, as opposed to the original idea of applying the fixed-point theorem to mere unprovability. The proof has very much the same flavor as the proof of the incompleteness theorem. Interestingly, it dates from the same year as the construction, due to Rosser, that eliminates the use of ω-consistency in the first Incompleteness Theorem; like the Speed-up Theorem of Gödel, Rosser’s construction exploits the issue of short and long proofs. Gödel never submitted a proof for the Speed-up Theorem. Over the years several related proofs were published, but the first full proof of Gödel’s original result was given only in 1994 by Sam Buss in his ‘On Gödel’s theorems on lengths of proofs I: Number of lines and speedups for arithmetic.’ (Buss 1994). Buss also gives a second proof of the theorem which avoids self-reference, following a technique due to Statman. Gödel measures the length of proofs by the number of formulas; but there are also other possibilities, such as the number of symbols in the proof. The case of the Speed-up Theorem where the length of proof is measured by the number of symbols was proved by Mostowski in 1952 (Mostowski 1982). For proofs of similar results see Ehrenfeucht and Mycieleski 1971, and Parikh 1971. Though both measures may be equally natural candidates for measuring the length of a proof, proving the theorem for length measured by the number of symbols avoids a technical complication introduced by the other measure: there are only finitely many proofs with a given number of symbols, whereas there are infinitely many proofs with a given number of formulas.