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.
Open access article: A formal proof of the Kepler conjecture.
###
Journal
Forum of Mathematics Pi