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
