Mathematicians deliver formal proof of Kepler Conjecture

June 16, 2017

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

Plague likely a Stone Age arrival to central Europe

November 22, 2017

A team of researchers led by scientists at the Max Planck Institute for the Science of Human History has sequenced the first six European genomes of the plague-causing bacterium Yersinia pestis dating from the Late Neolithic ...

How to cut your lawn for grasshoppers

November 22, 2017

Picture a grasshopper landing randomly on a lawn of fixed area. If it then jumps a certain distance in a random direction, what shape should the lawn be to maximise the chance that the grasshopper stays on the lawn after ...

Ancient barley took high road to China

November 21, 2017

First domesticated 10,000 years ago in the Fertile Crescent of the Middle East, wheat and barley took vastly different routes to China, with barley switching from a winter to both a winter and summer crop during a thousand-year ...

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.