Among the many ramifications of quantum computation for apparently distant fields of study are its implications for the notion of mathematical proof. Performing any computation that provides a definite output is tantamount to proving that the observed output is one of the possible results of the given computation. Since we can describe the computer’s operations mathematically, we can always translate such a computation into the proof of some mathematical theorem. This was the case classically too, but in the absence of interference effects it is always possible to keep a record of the steps of the computation, and thereby produce (and check the correctness of) a proof that satisfies the classical definition - as “a sequence of propositions each of which is either an axiom or follows from earlier propositions in the sequence by the given rules of inference”. Now we are forced to leave that definition behind. Henceforward, a proof must be regarded as a process — the computation itself — for we must accept that in future, quantum computers will prove theorems by methods that neither a human brain nor any other arbiter will ever be able to check step-by-step, since if the ‘sequence of propositions’ corresponding to such a proof were printed out, the paper would fill the observable universe many times over.
- Deutsch, Ekert, and Lupacchini
“Machines, Logic and Quantum Physics”