Last week I wrote a post about arithmetical theorems having very long proofs, and linked to an article on the SEP for the details. Today, me and my colleague Luca Manzoni realised that there is a much simpler proof; it is essentially the same proof described by Scott Aaronson for the uncomputability of the busy beaver function, and it holds for any undecidable, recursively axiomatisable theory *T* (that is, if there exists a recursive set of axioms generating the sentences of the theory, but no decision procedure for checking whether a sentence is a theorem).

Let *L*(*φ*) be the length in symbols of the shortest proof of the sentence *φ*, using a standard set of inference rules together with any recursive set of axioms for *T*; set *L*(*φ*) = 0 if *φ* is not a theorem. Also, let *L*(*n*) be the maximum *L*(*φ*) among all sentences *φ* of length at most *n*.

**Theorem.** *L* grows faster than any computable function.

*Proof.* Otherwise, given a sentence *φ*, we can first compute an integer *f* (|*φ*|) ≥ *L*(|*φ*|), then enumerate all proofs of length at most *f* (|*φ*|) and check them. If at least one of these is a proof of *φ*, we answer “yes”, otherwise “no”. But this is a decision procedure for *T*, since we know that if *φ* is a theorem, then it has a proof of length at most *f* (|*φ*|); contradiction. □

In particular, the theorem holds for Peano arithmetic and friends.