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\