Team announces construction of a formal computer-verified proof of the Kepler conjecture

Kepler conjecture
One of the diagrams from Strena Seu de Nive Sexangula, illustrating the Kepler conjecture
( —A team of researchers led by the man, Thomas Hales, who came up with written proof of the Kepler conjecture is now reporting that they have constructed a formal proof of the conjecture, which implies the use of a computer. The announcement was made on The Flyspeck Project page, and puts to rest any doubts about the correctness of the proof done by Hales in 1998.

It was back in 1611 that Johannes Kepler first suggested in a paper he'd written (after corresponding with Thomas Harriot) that if you want to stack cannon balls on a ship's deck in the most efficient way possible (a question originally posed by Sir Walter Raleigh), the best way to do it is in a pyramid shape. Cut to 1998 when Hales completed work on his written proof (which included portions that could only be verified by computer). But it was huge, as many tend to be—300 pages in all that took 12 reviewers four years to verify. A 99 percent certainty rating wasn't enough for Hales, however, so he launched the Flyspeck Project to create a means for proving the proof correct using a computer.

Hales and his team used two software tools that have been created for the sole purpose of verifying proofs—HOL Light and Isabelle—they work by checking the logic of statements made in the proof. Now after eleven years of work, the team has announced that they've succeeded in their endeavor. Hales' original proof has been converted to code the computer can work with and the software checkers found no discrepancies, which means the proof of the conjecture has been verified.

The success by the team highlights a growing movement of using computers to verify proofs that human beings have created giving the results more credence. Computers have also been used to construct original proofs for some basic problems, which suggests that someday in the not-too-distant future, computers will be doing all the heavy work, leaving mathematicians to ponder the deeper questions regarding what the proofs represent and how they can be used in real world applications.

Explore further

Computer generated math proof is too large for humans to check

More information: … AnnouncingCompletion

via Newscientist

© 2014

Citation: Team announces construction of a formal computer-verified proof of the Kepler conjecture (2014, August 13) retrieved 22 May 2019 from
This document is subject to copyright. Apart from any fair dealing for the purpose of private study or research, no part may be reproduced without the written permission. The content is provided for information purposes only.

Feedback to editors

User comments

Aug 13, 2014
How could you stack them any other way?

Aug 13, 2014
That would be something that would definitely be asked more often had this proof not been found to be true.

Aug 13, 2014
There's a number of interesting problems associated with packing algorithms (in what configuration do you need the least amount of packing material for a given amount of objects of a certain kind).
The 'easiest' are packages for spherical shapes (oranges, tennis balls, etc. )

An interesting result is that until 55 spheres the best packaging (highest density/least amount of wasted space between balls) is a tube. (This is why tennis balls come in tubular packages). After that number the best configuration switches to a cluster (and back to a tube for numbers 57, 58, 63 and 64...and no one can exactly explain why there is such a weird back and forth between 1D and 3D). Bizarrly enough there is no 2D optimal packaging configuration - ever.

Topologists refer to this number (jokingly) as a 'sausage catastrophe'.

Aug 13, 2014
Now that is cool! Thanks. I read something years ago about packing in 24 dimensions being much simpler, but I'm still trying to recover from trying to understand it...

I'm back, by the way. I was Dr_Toad. Now I'm my website. ;)

Aug 13, 2014
false, you melt the cannonballs down and reform them as needed in order to carry the most possible.

Please sign in to add a comment. Registration is free, and takes less than a minute. Read more