Summary: This paper puts forward a new notion of a proof based on computational complexity and explores its implications for computation at large.
Computationally sound proofs provide, in a novel and meaningful framework, answers to old and new questions in complexity theory. In particular, given a random oracle or a new complexity assumption, they enable us to (i) prove that verifying is easier than deciding for all theorems; (ii) provide a quite effective way to prove membership in computationally hard languages (such as \({\mathcal C}o\)-\(\mathcal N \mathcal P\)-complete ones); and (iii) show that every computation possesses a short certificate vouching its correctness.
Finally, if a special type of computationally sound proof exists, we show that Blum’s notion of program checking can be meaningfully broadened so as to prove that \(\mathcal N \mathcal P\)-complete languages are checkable.