The Changing Nature of Proof

PITTSBURGH-It used to be that a mathematical proof meant absolute certainty. But today's proofs often are so long and complex that it's practically impossible for anyone to read one, let alone verify it.

Thomas C. Hales, the University of Pittsburgh Mellon Professor of Mathematics, famously and finally proved Johannes Kepler's 400-year-old conjecture that the most efficient way to pack spheres was in a pyramid shape. However, when his proof was published in a peer-reviewed journal, reviewers said they could only be 99 percent certain that it was correct-one percent too little for the exacting Hales.

Hales now is using his problem-solving skills to "prove the proof" using a specially written computer language in what he calls the Flyspeck Project, which he will discuss at the annual meeting of the American Association for the Advancement of Science (AAAS) in St. Louis, Mo., in a session titled "Paradise Lost? The Changing Nature of Mathematical Proof," Saturday, Feb. 18, from 9:45 a.m. to 11:15 a.m. (C.S.T.).

Though the Kepler conjecture may seem intuitive, no one was able to create a formal proof of it until Hales astonished mathematicians across the world by doing so in 1998.

The computer-assisted proof filled more than 300 pages. An abridged version (a mere hundred-something pages) was published in November 2005 in Annals of Mathematics. The unabridged proof will be published in the July 2006 issue of Discrete and Computational Geometry.

"Computers have advanced to the point where it is now possible to go back and check every single logical inference, all the way back to the axioms, on relatively complicated mathematical proofs," said Hales. This means taking a traditional mathematical proof, which is written in English, and transcribing it into a form the computer can understand. Hales estimates that his proof of Kepler's conjecture will take about 20 "work-years" to transcribe (meaning, for example, if 10 people worked on it, it would take two years).

John Harrison, of Intel, wrote the computer code for the system used in the Flyspeck Project, called HOL (Higher Order Logic) Light. In December 2005, Tobias Nipkow, a professor at the Technical University of Munich, along with graduate students Gertrude Bauer and Paula Schultz, finished checking one of the major computer programs used in the proof, called Isabelle/HOL. Another of Nipkow's grad students, Steven Obua, is working on a verification of another major piece of computer code used in the proof; and Roland Zumkeller, a grad student at the Ecole Polytechnique in Paris, is making his thesis the verification of a third major piece of computer code.

In addition to Hales, the symposium, part of the daylong event "Beyond Pi: Grand Challenges in the Mathematical Sciences," will feature other mathematicians whose work challenges the very nature of proof: Keith Devlin of Stanford University, Michael Aschbacher of the California Institute of Technology, and Steven Krantz of Washington University.

The following week, Hales will deliver a lecture titled "Computers and the Future of Mathematical Proofs" Friday, Feb. 24, at 3:30 pm. in Room 2500 of Pitt's Wesley W. Posvar Hall, as part of the 46th annual lecture series of the University's Center for the Philosophy of Science.

Hales' research focuses in the areas of representation theory, discrete geometry, and honeycombs. He earned the Ph.D. degree in mathematics at Princeton University in 1986.

###

2/14/06/tmw