What's the densest way to pack spheres? Here are two equally good ways.
In fact there are infinitely many
equally good ways! We start by laying spheres on the plane in a hexagonal arrangement, as tightly as we can. Then we put a second layer like this on top, with the new spheres resting in the gaps between the old ones. Then we put on a third layer. But now there are 2 really different ways to do it!
The spheres in the third layer can be directly above
the spheres in the first layer - that's the picture at right. Or they can be not directly above
- shown at left.
As we continue, we keep getting more choices.
choice is to make the layers alternate like ABABAB..... That's called the hexagonal close packing
, and that's how crystals of magnesium work.
Another systematic choice makes every third
layer be the same, like ABCABC... That's called the cubic close packing
or face-centered cubic
, and that's how crystals of lead work.
(Why "cubic?" Because - even though it's not obvious! - you can also get this pattern by putting a sphere at each corner and each face of a cubical lattice. Trying to visualize this in your head is a great way to build your brain power.)
There are also uncountably many unsystematic
ways to choose how to put down the layers of spheres, like ABACBCAC.... You just can't use the same letter twice in a row.
In 1611, the famous astronomer Kepler conjectured that sphere packings of this sort were the densest possible. They fill up
π / 3 √2 = 0.740480489...
of the space, and he claimed you can't do better.
Proving this turned out to be very, very
hard. Wu-Yi Hsiang claimed to have a proof in 1993. It was 92 pages long. Experts said it had gaps (pardon the pun). Hsiang has never admitted there's a problem.
Thomas Hales claimed to have a proof in 1998. His proof took 250 pages... together with 3 gigabytes of computer programs, data and results!
The famous journal Annals of Mathematics
agreed to check his proof with a board of 12 referees. In 2003, after four years of work, the referees accepted his paper. But they didn't exactly say it was correct. They said they were "99% certain" it was right - but they didn't guarantee the correctness of all of the computer calculations.
Hales wasn't happy.
He decided to do a completely rigorous
proof using computer logic systems, so that automated proof-checking software could check it. He worked on it for about 10 years with a large team of people.
He announced that it was done on 10 August 2014. You can see it here:https://code.google.com/p/flyspeck/wiki/AnnouncingCompletion
To verify the proof, the main thing you need to do is check 23,000 complicated inequalities. Checking all these on the Microsoft Azure cloud took about 5000 processor-hours.
When it was done, Hales said:"An enormous burden has been lifted from my shoulders. I suddenly feel ten years younger!"
Personally I prefer shorter proofs. But this is quite a heroic feat.
I actually wrote about this because I want to talk about packing tetrahedra
. But I figured if you didn't know the more famous story of packing spheres
, that would be no good.
For more, check out Hales' free book, which starts with a nice history of the Kepler problem:
• Thomas C. Hales, Dense Sphere Packings: a Blueprint for Formal Proofs
For more on computer-aided proof, try this paper:
• Thomas C. Hales, Developments in formal proofs, http://arxiv.org/abs/1408.6474
The image here was created by Christophe Dang Ngoc Chan and the words translated to English by "Muskid":https://commons.wikimedia.org/wiki/File:Empilement_compact.svg #spnetwork