August 13, 2014 report

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

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 mathematical proofs 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

© 2014 Phys.org

**Citation**: Team announces construction of a formal computer-verified proof of the Kepler conjecture (2014, August 13) retrieved 22 May 2019 from https://phys.org/news/2014-08-team-formal-computer-verified-proof-kepler.html

## User comments

jackjumpViperSRT3gantialias_physorgThe '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'.

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

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