Probabilistically Checkable Proofs
Madhu Sudan
Microsoft Research
As advances in mathematics continue at the current rate, editors of mathematical journals increasingly face the challenge of reviewing increasingly long, and often wrong, ``proofs'' of classical conjectures. Often, even when it is a good guess that a given submission is erroneous, it takes excessive amounts of effort on the editor/reviewer's part to find a specific error one can point to. Most reviewers assume this is an inevitable consequence of the notion of verifying submissions; and expect the complexity of the verification procedure to grow with the length of the submission.
In this talk I will describe how research, mostly in the 20th century, has allowed us think about theorems and proofs formally; and how this formal thinking has paved the way for radically easy ways of verifying proofs. In particular I will introduce the "PCP" (for Probabilistically Checkable Proof) format of writing proofs. This is a format that allows for perfectly valid proofs of correct theorems, while any purported proof of an incorrect assertion will be ``evidently wrong'', so that a reviewer checking consistency of a very parts of the proof (probabilistically) will detect an error. The existence of PCPs may seem purely fictional but research since the 1990s has shown how such PCPs do exist. In this talk I will explain the concept of a PCP. After giving some some background on why theoretical computer scientists are interested in PCPs and theorems and proofs in general, I will attempt to give an idea of how such PCP formats, and associated verification methods are designed.