Mathematical proof is foolproof, it seems, only in the absence of fools
Enormous Theorems, Unwieldy Proofs
In recent years proof has become a surprisingly contentious topic. One thread of discord began with the 1976 proof of the four-color-map theorem by Kenneth Appel, Wolfgang Haken and John Koch of the University of Illinois at Urbana-Champaign. They showed that if you want to color a map so that no two adjacent countries share a color, four crayons are all you'll ever need. The proof relied on computer programs to check thousands of map configurations. This intrusion of the computer into pure mathematics was greeted with suspicion and even disgust. Haken and Appel reported a friend's comment: "God would never permit the best proof of such a beautiful theorem to be so ugly." Apart from such emotional and aesthetic reactions, there was the nagging question of verification: How can we ever be sure the computer didn't make a mistake?
Some of the same issues have come up again with the proof of the Kepler conjecture by Thomas C. Hales of the University of Pittsburgh (with contributions by his student Samuel P. Ferguson). The Kepler conjecture—or is it now the Hales-Ferguson theorem?—says that the pyramid of oranges on a grocer's shelf is packed as densely as possible. Computations play a major part in the proof. Although this reliance on technology has not evoked the same kind of revulsion expressed three decades ago, worries about correctness have not gone away.
Hales announced his proof in 1998, submitting six papers for publication in Annals of Mathematics. The journal enlisted a dozen referees to examine the papers and their supporting computer programs, but in the end the reviewers were defeated by the task. They found nothing wrong, but the computations were so vast and formless that exhaustive checking was impractical, and the referees felt they could not certify the entire proof to be error-free. This was a troubling impasse. Eventually the Annalspublished "the human part of the proof," excluding some of the computational work; the full proof was published last summer in Discrete and Computational Geometry. Interestingly, Hales has turned his attention to computer-assisted methods of checking proofs.
In the case of another famously problematic proof, we can't put the blame on computers. An effort to classify the mathematical objects known as finite simple groups began in the 1950s; the classification amounts to a proof that no such groups exist outside of five known categories. By the early 1980s the organizers of the project believed the proof was essentially complete, but it was scattered across 500 publications totaling at least 10,000 pages. Three senior authors undertook to revise and simplify the proof, bringing together the major ideas in one series of publications. The process, still unfinished, is testing the limits of the human attention span—and lifespan. (One of the leaders of the revision program died in 1992.)
If some proofs are too long to comprehend, others are too terse and cryptic. Four years ago the Russian mathematician Grigory Perelman announced a proof of the Poincaré conjecture. This result says—here I paraphrase Christina Sormani of Lehman College—that if a blob of alien goo can ooze its way out of any lasso you throw around it, then the blob must be nothing more than a deformed sphere, without holes or handles. Everyday experience testifies to this fact for two-dimensional surfaces embedded in three-dimensional space, and the conjecture was proved some time ago for surfaces (or "manifolds") of four or more dimensions. The hard case was the three-dimensional manifold, which Perelman solved by proving a more-general result called the geometrization conjecture.
Perelman's proof is not easy reading. Sormani explains its strategy as "heating the blob up, making it sing, stretching it like hot mozzarella and chopping it into a million pieces." I applaud the vividness of this description, and yet it has not helped me follow Perelman's logic. Given the difficulty of the work, others stepped in to explicate and elaborate, publishing versions of the proof considerably longer than the original. These were not popularizations aimed at the general public; they were meant to explain the mathematics to mathematicians. Controversy ensued. Were the explicators trying to claim a share of the glory? Did they deserve a share? In August Perelman was awarded a Fields Medal, the biggest prize in mathematics, which may put an end to the controversy. (Perelman refused the prize.)