New! Sign up for our free email newsletter.
Science News
from research organizations

Mathematicians deliver formal proof of Kepler Conjecture

June 16, 2017
Cambridge University Press
A mathematical problem more than 300 years old gets a formal proof with the help of computer formal verification.

A team led by mathematician Thomas Hales has delivered a formal proof of the Kepler Conjecture, which is the definitive resolution of a problem that had gone unsolved for more than 300 years. The paper is now available online through Forum of Mathematics, Pi, an open access journal published by Cambridge University Press. This paper not only settles a centuries-old mathematical problem, but is also a major advance in computer verification of complex mathematical proofs.

The Kepler Conjecture was a famous problem in discrete geometry, which asked for the most efficient way to cram spheres into a given space. The answer, while not difficult to guess (it's exactly how oranges are stacked in a supermarket), had been remarkably difficult to prove. Hales and Ferguson originally announced a proof in 1998, but the solution was so long and complicated that a team of a dozen referees spent years working on checking it before giving up.

Explains Henry Cohn, editor of Forum of Mathematics, Pi: "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. 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."

Thomas Hales is the Mellon Professor of Mathematics at the University of Pittsburgh. His research spans discrete geometry, representation theory, motivic integration, and formal theorem proving.

Story Source:

Materials provided by Cambridge University Press. Note: Content may be edited for style and length.

Journal Reference:

  1. Roland Zumkeller et al. A FORMAL PROOF OF THE KEPLER CONJECTURE. Forum of Mathematics, Pi, 2017; 5 DOI: 10.1017/fmp.2017.1

Cite This Page:

Cambridge University Press. "Mathematicians deliver formal proof of Kepler Conjecture." ScienceDaily. ScienceDaily, 16 June 2017. <>.
Cambridge University Press. (2017, June 16). Mathematicians deliver formal proof of Kepler Conjecture. ScienceDaily. Retrieved December 5, 2023 from
Cambridge University Press. "Mathematicians deliver formal proof of Kepler Conjecture." ScienceDaily. (accessed December 5, 2023).

Explore More
from ScienceDaily