Mathematicians deliver formal proof of Kepler Conjecture

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


Explore further

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

More information: Thomas Hales et al, A Formal Proof of the Kepler Conjecture, Forum of Mathematics, Pi (2017). DOI: 10.1017/fmp.2017.1
Citation: Mathematicians deliver formal proof of Kepler Conjecture (2017, June 16) retrieved 17 August 2019 from https://phys.org/news/2017-06-mathematicians-formal-proof-kepler-conjecture.html
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.
230 shares

Feedback to editors

User comments

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