Pitt professor solves math mystery

It started with a snowflake and became one of the world’s greatest mathematical mysteries.

Four centuries later and that mystery was solved by a professor now residing at Pitt.

Andrew W. Mellon Professor of Mathematics Thomas C. Hales has been selected by the American Mathematical Society to be an inaugural fellow in 2013. AMS is the world’s largest society dedicated to “further the interests of mathematical research and scholarship,” according to its mission statement.

Hales earned this distinction for his work on the Kepler Conjecture, a statement about sphere packing that, though regarded as accurate, had never been mathematically proven — until now.

Hales and graduate student Samuel Ferguson announced the breakthrough back in 1998 while working at the University of Michigan. But it was only in 2006, after a panel of 12 referees became exhausted in their attempt to check Hales’ work, that a journal allowed its publication in the Annals of Mathematics. The entire process was highly unusual.

“When you see a problem that’s gone unsolved for 400 years, you get lured in by how easy it seems,” Hales said. “By the time I realized the difficulty of it, I was hooked.”

Hales recounted the extensive process that led to the conjecture’s proof. The story began long before the conjecture’s namesake, Johannes Kepler, entered the picture, with a conversation in the late 1590s between two men: Sir Walter Raleigh and Thomas Harriot.

Raleigh, an English aristocrat, adventurer, author and poet, was about to embark on a sea voyage and needed some organizational assistance. He turned to Harriot, a renowned astronomer and mathematician, and asked the best way to stack cannonballs on a ship.

Harriot, one of the initial believers of the atomic theory, began corresponding with his friend, Kepler.

Kepler, a German scholar, had already made a name for himself in the fields of mathematics and astronomy, postulating laws of planetary motion.

Kepler was unconvinced by the similarities between the cannonball concept and the newfangled atomic theory that was milling about until he was walking down an alley and saw a six-sided snowflake.

Then, everything changed.

Kepler began to think of the snowflake’s structure and the internal arrangements that led to its hexagonic nature. Kepler proposed the cannonball arrangement in 1611 as the densest method of sphere packing — the same method grocers frequently utilize when stacking oranges or other spherical edibles.

However, Kepler couldn’t prove his own idea.

“The Kepler conjecture is famous partly because it took so long to prove and because many great mathematicians attacked the problem over the centuries without success or with partial success. [Sir Isaac] Newton and [Carl Friedrich] Gauss both worked on it and brought some insight into the problem but couldn’t solve it,” said Ivan Yotov, the chair of Pitt’s mathematics department.

In 1900, the famous mathematician David Hilbert named the conjecture on his list of 23 problems in mathematics. Hilbert’s list of unsolved conjectures directed the field for much of the 20th century.

The problem seems simple enough but was nearly impossible to prove. There were innumerable possibilities in arranging the spheres, and to solve the conjecture, Hales would have to go through each one.

“The increase in the power of computers led to the ability to solve it. Computers had to run for three months to generate the solution,” Hale said.

Yotov expounded on the importance of computers in proving the conjecture.

“Professor Hales’ proof is based on reducing the infinitely many possibilities to about 5,000 that potentially could be better. He then eliminates them one by one by using a sophisticated computer program,” Yotov said. “This is a fascinating example of combining traditional pen-and-paper mathematical arguments with computations.”

Even when the 300-page proof was submitted in 1998, the process was far from finished. Each year the dozen referees would return to Hales, informing him that they were 99 percent certain it was correct but needed more time. Finally, in 2006, they pled exhaustion and formally announced they were 99 percent certain of the proof’s correctness. The journal accepted Hales’ work and published the proof.

But Hales was unsatisfied.

“This was ridiculous. Math should be cut and dry. You shouldn’t have to wait years and years. I thought, there’s gotta be a better way,” Hales said.

And so began the Flyspeck Project, a project aimed to act as an artificial referee by completely checking the accuracy of a proof. Under the project, a formal proof is created, which differs from a traditional one in that every intermediate step is provided with no jumps left up to intuition. Because it is less intuitive, the formal proof is less susceptible to logical errors.

Hales is close to the project’s completion now, which would allow for 100-percent certainty in regard to his proof.

Although the program would “still require a certain amount of human interaction,” Hales said, it has far-reaching applications.

Flyspeck could be used to check the accuracy of computer encoding on chips, thereby preventing costly recalls such as that of Intel’s mishap in 1994, which cost over $400 million. The bug had significant repercussions because of the incorrect divisions it caused.

The program could also be used for the monitoring of aircraft software or automobile braking systems. Sphere packing itself is important for engineers, as well as for error-correcting codes.

Hales’ recently published book, “Dense Sphere Packings: A Blueprint for Formal Proofs,” demonstrates the new “proving of the proof” along with additional conjecture solutions in discrete geometry.

“The resolution of the Kepler Conjecture is one of the most important developments in discrete and computational geometry in the last century,” Yotov said.