But now note that since \(n\text{-}\sc{PROVABILITY}_{\mathsf{T}} \in \textbf{NP}\), if it so happened that \(\textbf{P} = \textbf{NP}\) then the task of determining whether a mathematical formula is derivable in our preferred mathematical theory by a proof of feasible length would be checkable by an efficient algorithm. Gödel suggests that this would have the following consequence: