24 February 2006
Packing Oranges and Proving Theorems

Nothing, it seems, can resist the advance of the computers. Another bastion of the ages is falling to them. Since the time of Euclid, what it took to prove a proposition has remained essentially the same. You wonder if the square on the hypotenuse is equal to the sum of... well you know. To assure yourself that it is so, you trace through Euclid's proof. A few well chosen constructions here, the similarity of this or that triangle, and soon enough even the most skeptical must admit the proposition.

That is how it went for two thousand years. The mathematics got harder and the proofs longer. But the method stayed the same. A proof was a long series of propositions to be pored over, checking step by step that this follows from that until the final theorem emerges. Archimedes did it by tracing figures in the sand with a sharp stick. More recently, mathematicians use a pencil and paper.

Of course there were a few recalcitrant problems. In 1611 Kepler conjectured that the most oranges could be stacked in some space if we stack them just the way green grocers have been doing it since anyone can remember. Over four hundred years later no one had found a proof for this conjecture. This was no simple problem.

Along comes Tom Hales, now Mellon Professor of Mathematics at the University of Pittsburgh, and he proves it. The proof took over a decade to find and fills hundreds of pages. But even those pages are not the entirety of the proof. Time and again throughout it, Hales had so many "this follows from that" to check that it proved impossible to write them all out. He had to use a computer to do it.

The result was a very different sort of proof. When he sent it to a journal for publication, he and his collaborator needed to mount a week long seminar to explain to the four referees chosen by the journal just how the proof worked. And even a year later, they were able to report that they were only 99% certain of the correctness of the proof.

This, Hales told us, at his Annual Lecture Series Presentation of February 24, 2006, is just the beginning of a new age. He is now part of a new movement proving theorems of such complexity that only a computer can do it. And the movement brings a new rigor to old proofs. They are translated into the language of the computer and the computer checks them line by line.

In this new era, the essential tools of the mathematician are no longer just Archimedes' sand or pencil and paper. Mathematicians now need high speed computers with huge memories to help them check new universes of "this follows from that." Indeed the access to very high speed computers was one of the things that attracted Hales to Pittsburgh. After two thousand years, Euclid would not longer recognize the desk of a working mathematician, for it is now the virtual desktop.

John D. Norton

Thomas Hales
Friday, 24 February 2006
::: Computers and Future of Mathematical Proofs
::: Annual Lecture Series