  The generally accepted wisdom in computational circles is that pure proof
verification is a solved problem and that the computationally hard elements and
fertile areas of study lie in proof discovery. This wisdom presumably does hold
for conventional proof systems such as first-order logic with a standard proof
calculus such as natural deduction or resolution. But this folk belief breaks
down when we consider more user-friendly/powerful inference rules. One such
rule is the restricted {\omega}-rule, which is not even semi-decidable when
added to a standard proof calculus of a nice theory. While presumably not a
novel result, we feel that the hardness of proof verification is
under-appreciated in most communities that deal with proofs. A proof-sketch
follows.
