Mathematicians deliver formal proof of Kepler Conjecture

June 16, 2017, Cambridge University Press

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

Related Stories

Mathematician announces that he's proved the ABC conjecture

September 12, 2012

(Phys.org)—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 ...

Recommended for you

Ancient mice discovered by climate cavers

September 24, 2018

The fossils of two extinct mice species have been discovered in caves in tropical Queensland by University of Queensland scientists tracking environment changes.

The first predators and their self-repairing teeth

September 24, 2018

The earliest predators appeared on Earth 480 million years ago—and they even had teeth capable of repairing themselves. A team of palaeontologists led by Bryan Shirley and Madleen Grohganz from the Chair for Palaeoenviromental ...

Fat from 558 million years ago reveals earliest known animal

September 20, 2018

Scientists from The Australian National University (ANU) and overseas have discovered molecules of fat in an ancient fossil to reveal the earliest confirmed animal in the geological record that lived on Earth 558 million ...

0 comments

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.