homehome Home chatchat Notifications


Mathematicians deliver formal proof of Kepler's conjecture

Kepler published this conjecture in 1611. Now, the human mind and computer algorithms have managed to solve it.

Mihai Andrei
June 19, 2017 @ 7:48 pm

share Share

What do stacked oranges have in common with a mathematical conjecture that’s been unproven for 300 years? At a first glance, not much…

Image in Public Domain.

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.

Prof. Hales demonstrates his solution to the Kepler conjecture. Image credit: Bob Kalmbach / University of Michigan.

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

share Share

China Resurrected an Abandoned Soviet 'Sea Monster' That's Part Airplane, Part Hovercraft

The Soviet Union's wildest aircraft just got a second life in China.

A Rocket Carried Cannabis Seeds and 166 Human Remains into Space But Their Capsule Never Made It Back

The spacecraft crashed into the Pacific Ocean after a parachute failure, ending a bold experiment in space biology and memorial spaceflight.

Ancient ‘Zombie’ Fungus Trapped in Amber Shows Mind Control Began in the Age of the Dinosaurs

The zombie fungus from the age of the dinosaurs.

Your browser lets websites track you even without cookies

Most users don't even know this type of surveillance exists.

What's Seasonal Body Image Dissatisfaction and How Not to Fall into Its Trap

This season doesn’t have to be about comparison or self-criticism.

Why a 20-Minute Nap Could Be Key to Unlocking 'Eureka!' Moments Like Salvador Dalí

A 20-minute nap can boost your chances of a creative breakthrough, according to new research.

The world's oldest boomerang is even older than we thought, but it's not Australian

The story of the boomerang goes back in time even more.

Swarms of tiny robots could go up your nose, melt the mucus and clean your sinuses

The "search-and-destroy” microrobot system can chemically shred the resident bacterial biofilm.

What if Every Roadkill Had a Memorial?

Road ecology, the scientific study of how road networks impact ecosystems, presents a perfect opportunity for community science projects.

Fireball Passes Over Southeastern United States

It’s a bird! It’s a plane! It’s… a bolide!