We are, of course, generally interested in the question of whether \(\phi\) is provable in \(\mathsf{T}\) without a restriction on the length of its derivation – e.g. in the case where \(\phi\) expresses the Riemann Hypothesis and \(\mathsf{T}\) is a theory like \(\textsf{ZFC}\). But in a letter to von Neumann, Gödel (1956) observed that if we were able to efficiently decide \(n\text{-}\sc{PROVABILITY}_{\mathsf{T}}\), then this would already have enormous significance for mathematical practice. For note that it seems plausible to assume that no human mathematician will ever be able to comprehend a proof containing 100 million symbols (\(\approx 25000\) pages). If we were able to efficiently check if \(\phi \in n\text{-}\sc{PROVABILITY}_{\mathsf{T}}\) (say for \(n = 10^8\)) and obtained a negative answer, Gödel concludes that “there would be no reason to think further about [\(\phi\)]” (1956, p. 612). For in this case a demonstration that \(\phi \not\in n\text{-}\sc{PROVABILITY}_{\mathsf{T}}\) (for a sufficiently large \(n\) and a sufficiently powerful \(\mathsf{T}\)) would be sufficient to show that we have no hope of ever comprehending a proof of \(\phi\) even if one were to exist.