Holographic proofs: keeping computers and mathematicians honest

Science News, June 6, 1992 by Ivars Peterson

After years of scrupulous reasoning and painstaking analysis, Peter Fermax of Enormous State University truly believed he had proved the infamous Snark Conjecture. Now he faced the formidable task of persuading his fellow mathematicians that his 1,210-page manuscript contained not a single error that would invalidate the proof.

Who would have the time and patience to check each line and certify the proof's integrity?

Unlike his mathematical forebears, who typically had to struggle mightily to win acceptance of their lengthy proofs, Fermax had a tool at his disposal that greatly eased a proof checker's burden. Having already expressed his long chain of reasoning in an acceptable, logical form, he could call upon a supercomputer to convert his statements automatically into a "holographic" version of the same proof.

As in a laser-generated hologram, which makes possible the reconstruction of a scene not only from the whole recorded image but also from each tiny subsection of the image, every statement in a holographic proof contains information about the entire proof. Thus, an error in even a single line of the original proof has a high probability of showing up in any given line of the holographic proof.

In effect, converting a proof into its holographic form greatly amplifies any mistakes present and makes them more readily detectable. To ascertain a proof's validity, a checker has merely to examine, say, a few dozen statements. There's no need to look at the whole proof -- no matter how long.

Confident that his proof would withstand scrutiny, Fermax submitted the holographic version to the editors of an electronic journal. Using a rudimentary desktop computer, an anonymous reviewer quickly checked the proof, and the Snark Conjecture became the Fermax Theorem.

Although such a scenario presently exists more in the realm of fantasy than in the real world, computer scientists have over the last few years established the basic principles underlying this sort of scheme. Recent advances in theoretical computer science already point to a remarkably powerful means of checking the correctness of specific answers supplied by a computer.

Quite unexpectedly, the same advances also provide important insights into the strict limits that researchers face when attempting to compute even approximate answers to a variety of problems in computer science. They now know that if it takes an unrealistically long time to compute the exact solutions of certain problems that involve choosing optimal strategies from a host of possibilities, then finding acceptable approximate answers will encounter the same barrier.

"This is something that follows in the best traditions of mathematics, where the beauty and the power of a new method comes from connecting things that don't resemble one another," says computer scientist Laszlo Babai of the University of Chicago.

"These are really crucial developments," agrees Leonid Levin of Boston University.

Babai and Levin were among the professors and students at a number of institutions who contributed to the chain of results that led to this convergence between proof checking and the complexity, or difficulty, of computing answers to certain problems.

Moreover, once computer scientists hurdle some of the obstacles in these theoretical results, "I think they may have dramatic practical consequences," Levin says.

At the root of these developments lies the startling notion of a probabilistic, interactive proof. Unlike traditional methods -- familiar to any student who has tried to prove one of Euclid's geometrical theorems by constructing a chain of statements inexorably leading to the necessary conclusion -- this new technique relies on randomness and the interplay between a "prover" and a "checker" to achieve a practically unassailable proof.

"What is new and very different is that one can convince somebody [of a proof's validity] by using coin flipping and interaction," says Manuel Blum of the University of California, Berkeley, who played a leading role in developing this concept. "I'm excited about that because I think theoretical computer science has introduced a new paradigm here -- a paradigm proving to be very powerful for many different reasons and purposes."

Computer scientists several years ago used this concept as the basis for the wonderfully counterintuitive notion of a "zero-knowledge proof." Such a scheme permits someone to persuade others that a particular theorem she has proved is true without giving away anything about how to go about proving the theorem itself (SN: 8/30/86, p. 140).

Blum has applied the concept of interactive proofs to what he terms "result checking" or "program checking."

Computer scientists normally count on two methods for ensuring the reliability of computer programs. They can mathematically prove that a given program works correctly for all possible inputs, but that's usually very difficult, if not infeasible. Alternatively, they can test the program by feeding it various inputs, but in this case there's no assurance that the tests cover all the types of inputs a program may encounter.