review articles

Doi: 10.1145/1467247.1467267

novel formats for writing proofs of

Can a proof be checked without reading it? ^{mathematical assertions. Associated}
with these formats are probabilistic al-
gorithms that reviewers could (should?)
BY maDhu suDan
use to verify the proofs. A reviewer using
such a verification algorithm would be
spared from reading the entire proof

Probabilistically

(and indeed will only read a “constant number of bits of the proof”—a notion we will elaborate on, and explain later). Any researcher who has a proof of a the-

checkable
orem can rewrite the proof in the pre-
scribed format and offer it to the review-
er, with the assurance that the reviewer
will be convinced of this new proof. On
Proofs
the other hand, if someone claims a
faulty assertion to be a theorem, and
offers any proof (whether in the new for-
mat or not), the reviewer will discover an
error with overwhelming probability.

In what follo ws we will attempt to formalize some of the notions that we have been using in a casual sense above. The central notion that will emerge is that of a “probabilistically checkable proof (PCP).” Existence of such formats and verification algorithms often runs contrary to our intuition. Nevertheless they do exist, and we will discuss two different approaches that have been used thus far to construct such PCPs.

PCPs are arguably fascinating objects. They offer a certain robustness to the logical process of verification that may not have been suspected before. While the process of proving and verifying theorems may seem of limited interest (say, only to mathematicians), we stress that the notion of a “ convincing” argument/evidence applies much more broadly in all walks of life. PCPs introduce the fascinating possibility that in all such cases, the time taken to assess the validity of the evidence in supporting some claims may be much smaller than the volume of the evidence. In addition to this philosophical interest in PCPs, there is a very different (and much more concrete) reason to study PCPs. It turns out that PCPs shed light in the area of combinatorial optimization. Unfortunately this light is “dark”: The ability to construct PCPs mostly says that for many optimization

the taSK oF

verifying a mathematical proof is extremely

onerous, and the problem is compounded when a reviewer really suspects a fatal error in the proof but still has to find an explicit one so as to convincingly reject a proof. Is there any way to simplify this task? Would not it be great if it were possible to scan the proof cursorily (such as, flip the pages randomly, reading a sentence here and a sentence there) and be confident that if the proof was buggy you would be able to find an error by such a superficial reading?

Alas, the current day formats of proofs do not allow such simple checks. It is possible to build a “proof” of any “assertion” (in particular ones that are not true) with just one single error, which is subtly hidden. Indeed, if you think back to the “proofs” of “ 1 = 2” that you may have seen in the past, they reveled in this flaw of current proof systems.

Fortunately this shortcoming of proofs is not an
inherent flaw of logic. Over the past two decades,
theoretical computer scientists have come up with