# Mathematicians deliver formal proof of Kepler Conjecture

June 16, 2017A 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.

-end-

Cambridge University Press

**Related Mathematics Articles:**

More democracy through mathematics

For democratic elections to be fair, voting districts must have similar sizes.

For democratic elections to be fair, voting districts must have similar sizes.

How to color a lizard: From biology to mathematics

Skin color patterns in animals arise from microscopic interactions among colored cells that obey equations discovered by Alan Turing.

Skin color patterns in animals arise from microscopic interactions among colored cells that obey equations discovered by Alan Turing.

Mathematics supports a new way to classify viruses based on structure

New research supports a structure-based classification system for viruses which could help in the identification and treatment of emerging viruses.

New research supports a structure-based classification system for viruses which could help in the identification and treatment of emerging viruses.

US educators awarded for exemplary teaching in mathematics

Janet Heine Barnett, Caren Diefenderfer, and Tevian Dray were named the 2017 Deborah and Franklin Tepper Haimo Award winners by the Mathematical Association of America (MAA) for their teaching effectiveness and influence beyond their institutions.

Janet Heine Barnett, Caren Diefenderfer, and Tevian Dray were named the 2017 Deborah and Franklin Tepper Haimo Award winners by the Mathematical Association of America (MAA) for their teaching effectiveness and influence beyond their institutions.

Authors of year's best books in mathematics honored

Prizes for the year's best books in mathematics were awarded to Ian Stewart and Tim Chartier by the Mathematical Association of America (MAA) on Jan.

Prizes for the year's best books in mathematics were awarded to Ian Stewart and Tim Chartier by the Mathematical Association of America (MAA) on Jan.

The mathematics of coffee extraction: Searching for the ideal brew

Composed of over 1,800 chemical components, coffee is one of the most widely-consumed drinks in the world.

Composed of over 1,800 chemical components, coffee is one of the most widely-consumed drinks in the world.

Even physicists are 'afraid' of mathematics

Physicists avoid highly mathematical work despite being trained in advanced mathematics, new research suggests.

Physicists avoid highly mathematical work despite being trained in advanced mathematics, new research suggests.

Mathematics and music: New perspectives on the connections between these ancient arts

World-leading experts on music and mathematics present insights on the connections between these two ancient arts, especially as they relate to composition and performance, as well as creativity, education, and geometry.

World-leading experts on music and mathematics present insights on the connections between these two ancient arts, especially as they relate to composition and performance, as well as creativity, education, and geometry.

Kindergarteners' mathematics success hinges on preschool skills

In a study funded by the National Science Foundation, researchers at the University of Missouri discovered that preschoolers who better process words associated with numbers and understand the quantities associated with these words are more likely to have success with math when they enter kindergarten.

In a study funded by the National Science Foundation, researchers at the University of Missouri discovered that preschoolers who better process words associated with numbers and understand the quantities associated with these words are more likely to have success with math when they enter kindergarten.

First international mathematics research institute launched in Australia

World leaders in the mathematical sciences are visiting Melbourne for a series of research programs at Australia's first international research institute for mathematics and statistics.

World leaders in the mathematical sciences are visiting Melbourne for a series of research programs at Australia's first international research institute for mathematics and statistics.

**Related Mathematics Reading:**

## Best Science Podcasts 2019

We have hand picked the**best science podcasts**for 2019. Sit back and enjoy new science podcasts updated daily from your favorite science news services and scientists.

**Now Playing: TED Radio Hour**

**Digital Manipulation**

Technology has reshaped our lives in amazing ways. But at what cost? This hour, TED speakers reveal how what we see, read, believe â even how we vote â can be manipulated by the technology we use. Guests include journalist Carole Cadwalladr, consumer advocate Finn Myrstad, writer and marketing professor Scott Galloway, behavioral designer Nir Eyal, and computer graphics researcher Doug Roble.

**Now Playing: Science for the People**

**#529 Do You Really Want to Find Out Who's Your Daddy?**

At least some of you by now have probably spit into a tube and mailed it off to find out who your closest relatives are, where you might be from, and what terrible diseases might await you. But what exactly did you find out? And what did you give away? In this live panel at Awesome Con we bring in science writer Tina Saey to talk about all her DNA testing, and bioethicist Debra Mathews, to determine whether Tina should have done it at all. Related links: What FamilyTreeDNA sharing genetic data with police means for you Crime solvers embraced...