What do stacked oranges have in common with a mathematical conjecture that’s been unproven for 300 years? At a first glance, not much…
What’s the best way to stack apples or oranges? Or to put it mathematically, what’s the best way of arranging equally sizes spheres in a three-dimensional Euclidian space? Intuitively, you’d say something like the image above, and you’d be right. The cubic close packing and hexagonal close packing arrangements yield the best density, at around 74%.
Johannes Kepler, the famous mathematician and astronomer predicted this 300 years ago, but he couldn’t prove it. No one could, actually; no one proved it for 300 years, until 1998, when Thomas Callister Hales, one of the world’s leading mathematicians, submitted a computer-aided proof. He opted for a “proof by exhaustion” — a brute force method which splits the problem into a possible number of cases and then analyzes all those cases.
The thing is, his initial proof was so complex that no one really got it, at least not at first. His proof consisted of 250 pages of notes and 3 gigabytes of computer programs, data and results. Keep in mind that this was 1998. Despite the unusual nature of the proof, the editors of the Annals of Mathematics agreed to publish it, after setting up a referee panel of 12 prominent mathematicians. It took them four years to reach a conclusion, saying that they are 99% of the validity of the proof, but could not verify all the individual calculations.
By all standards, it appeared to be a valid but unsatisfying proof, as Henry Cohn, editor of Forum of Mathematics, Pi, explains:
“The verdict of the referees was that the proof seemed to work, but they just did not have the time or energy to verify everything comprehensively. The proof was published in 2005, and no irreparable flaws were ever identified, but it was an unsatisfactory situation that the proof was seemingly beyond the ability of the mathematics community to check thoroughly.”
So Hales didn’t just move on to other things, he continued to keep an eye on a more elegant proof for this conjecture. He started work on a project called Flyspeck (you can check it out yourself, it’s open), with the F, P, and K, standing for Formal Proof of Kepler. Hales estimated that it would take 20 years to establish the proof, but it came much faster than anticipated.
Alongside 21 collaborators, he submitted a new, revised proof in 2015 — which was now approved and published, much faster than the initial one. Cohn explains:
“To address this situation and establish certainty, Hales turned to computers, using techniques of formal verification. He and a team of collaborators wrote out the entire proof in extraordinary detail using strict formal logic, which a computer program then checked with perfect rigor. This paper is the result of their completed work.”
I’ll try to save some dignity and not pretend to understand the proof. By all accounts, there’s only a handful of people in the world who can understand even this “simplified” proof. Instead, let’s focus on the significance (both practical, and historical) of this study.
There are several practical applications to proving this conjecture. For starters, it could help researchers understand the atomic distribution of crystals, and it could extend some 2D applications into a 3D space. The proof itself and the algorithms built could help mathematicians solve other complex problems.
Kepler’s conjecture is the oldest unsolved problem in discrete geometry; or rather, it was. Kepler wrote about it in 1611, in an essay called ‘On the six-cornered snowflake.’ It’s a perfect example of a solution which seems easy to find, but extremely difficult to prove. This new paper not only stifles a centuries-old debate, but shows just how well the human intellect and computer algorithms can work together. Modern mathematics can be a bizarre and frightening world, but things like this certainly make it much more exciting.
Journal Reference: Thomas Hales et al — A formal proof of the Kepler Conjecture. DOI: https://doi.org/10.1017/fmp.2017.1