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

August 13, 2014 by Bob Yirka, report

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

Related Stories

Mathematician announces that he's proved the ABC conjecture

September 12, 2012

(—In all of history there are very few names that stand out in the field of mathematics, at least among those not in the field: Euclid, Newton, Pythagoras, etc. This is likely due to several reasons, chief among ...

Detecting program-tampering in the cloud

September 11, 2013

For small and midsize organizations, the outsourcing of demanding computational tasks to the cloud—huge banks of computers accessible over the Internet—can be much more cost-effective than buying their own hardware. But ...

'Zero knowledge' may answer computer security question

August 29, 2013

( —In the age of the Internet, it's getting harder and harder to keep secrets. When you type in your password, there's no telling who might be watching it go by. New research at Cornell may offer a pathway to more ...

Recommended for you

Excavators find tombs buried in Bolivia 500 years ago

November 17, 2018

Archaeologists say they found tombs at a Bolivian quarry containing remains from more than 500 years ago that give an insight into the interaction of various peoples with the expanding Inca empire.

Preventing chemical weapons as sciences converge

November 15, 2018

Alarming examples of the dangers from chemical weapons have been seen recently in the use of industrial chemicals and the nerve agent sarin against civilians in Syria, and in the targeted assassination operations using VX ...


Adjust slider to filter visible comments by rank

Display comments: newest first

not rated yet Aug 13, 2014
How could you stack them any other way?
not rated yet Aug 13, 2014
That would be something that would definitely be asked more often had this proof not been found to be true.
5 / 5 (6) 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'.
3 / 5 (2) 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. ;)
not rated yet 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

Click here to reset your password.
Sign in to get notified via email when new comments are made.