**Packing spheres**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.

One

*systematic* 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/AnnouncingCompletionTo 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*,

https://flyspeck.googlecode.com/svn/trunk/kepler_tex/DenseSpherePackings.pdf.

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 arXiv:1408.6474

#formalProofs