From: "C. Hillman" <optimist@u.washington.edu>
Newsgroups: sci.math
Subject: Re: Mathematicians proves what the grocers already knew!
Date: Thu, 27 Aug 1998 01:13:10 -0700

On Thu, 27 Aug 1998, Virgil wrote:

> I just came in. 
> What is it that the grocers knew?

Someone in my department has posted the latest Science News, which
summarizes the situation. 

Prof. Thomas Hales (Math, Univ. of Michigan) and his graduate student
Samuel P. Ferguson have apparently used computers to prove the famous
Kepler conjecture (1611), which states that the densest packing of
identical balls in E^3 is the classical face-centered cubic packing.
(Gauss proved this is the densest -lattice- packing; the problem is to
show it is the densest of -all- such packings.)  I repeat, this problem
has been unsolved since 1611 (compare say 1650 for Fermat's last theorem),
so by standards of venerability it ought to be even bigger news than
Wiles' proof of FLT, although that was an "insight" proof and this is a
"brute force" proof. 

This is a very famous problem, probably the most famous in discrete
geometry.  Many announcments of proofs have been made over the years, and
all turned out to be wrong.  In particular, in 1993, Hsiang announced a
proof which met with some initial scepticism and was soon shot down by
alert critics. 

However, the Science News article adds a very important detail--- John
Horton Conway, a leading expert on lattices (see the book by Conway and
Sloane on sphere packings), has said that the proof outline is reasonable
and that Hales and Ferguson have taken all appropriate care to document
their code (even writing crucial pieces independently and running both
programs), so that it is reasonable to think that spot checks will not
uncover any errors.  Conway adds the conjecture that a short
"human-comprehensible" proof can perhaps be found. 

It is interesting that Fejes-Toth (who reduced the problem to a finite
minimization problem, too difficult for hand computation) speculated in
the fifties that this problem might eventually be solved by a brute force
computation. 

See

http://www.math.lsa.umich.edu/~hales/countdown/

for more information.

It is also interesting that despite the importance of the result,
mathematicians are unlikely to honor the authors for such a "brute-force" 
approach ;-)  Still, if it holds up, this would be another striking
example (cf. the four color theorem) of an apparently very hard problem
whose only known solution makes use of a vast and intricate brute-force
computation.  The complaint mathematicians have about such proofs is that
they tell you, more or less, that it is so, but don't leave you with any
feeling that you know -why- it is so. 

Chris Hillman

Please DO NOT email me at optimist@u.washington.edu.  I post from this account
to fool the spambots; human correspondents should write to me at the email
address you can obtain by making the obvious deletions, transpositions,
and insertion (of @) in the url of my home page:

   http://www.math.washington.edu/~hillman/personal.html

Thanks!