## The shortest proof for every theorem

Suppose we want to show that there is a number $$n$$ such that no upper bound on the busy beaver number $$\Sigma(n)$$ is provable from, say, the axioms of ZFC. One possible proof is as follows: Assume that no such $$n$$ exists. That is, assume that for every $$n$$, there is a proof in first-order logic that uses only the axioms of ZFC and derives a sentence $$\Sigma(n) \leq m$$ for some $$m$$. Then we could compute an upper bound for $$\Sigma(n)$$ by exhaustively searching all of the possible valid ZFC proofs until we found one that deduced a theorem of the form $$\Sigma(n) \leq m$$; by assumption, we must eventually find such a proof. But we know that we cannot compute an upper bound on $$\Sigma(n)$$ for arbitrary $$n$$; thus, we have derived a contradiction, and the original assumption must be false.

Enumerating proofs until you find one with the desired properties is one of those grand CS traditions that, like calling an $$O(n^{12})$$ algorithm “efficient” while dismissing an $$O(1.001^n)$$ algorithm as “intractable”, is handy for theoretical purposes but has essentially no bearing on the real world whatsoever. After all, no one would really write a program that loops through all possible proofs and tests each one.