Thomas Hales: The Proof of the Proof

The message went out without fanfare on a quiet summer morning. Thomas Hales finally was done—or so it seemed.

Near collapse, he e-mailed his colleagues announcing that he had achieved the impossible.

After more than a decade of work, Hales had completed a proof of the Kepler conjecture, a centuries-old conundrum about how best to pack together three-dimensional spheres that has eluded all attempts at solution by some of history’s grandest thinkers.

Hales’ proof of this famous geometric puzzle was a mathematical epic composed of 300 pages of traditional logic and 40,000 lines of computer code. His data files required more than 3 gigabytes of storage space — enough to fill an equal number of pickup trucks with books.

“The results are still preliminary in the sense that they have not been refereed and have not even been submitted for publication, but the proofs are to the best of my knowledge correct and complete,” Hales wrote in his e-mail on Aug. 9, 1998.

Then the young mathematician left for a month in Germany — his first true vacation since committing himself to cracking the Kepler conjecture four years beforehand.

“I’ve described it as crawling across the finish line of a marathon,” said Hales, the Andrew Mellon professor of mathematics at the University of Pittsburgh.

“It was total exhaustion, and release from that exhaustion,” Hales added.

But the release never really came.

A mathematical proof has a well-defined structure and set of conventions. It starts with accepted truths called axioms and uses a sequence of logic to arrive at a conclusion. If each assertion in the sequence is correct, then so is the end result.

Proofs must go through a rigorous process of peer review to determine whether they are

complete, correct and original — that is, fit to be published.

A dozen mathematicians who spent four years vetting Hales’ proof for the field’s most prestigious journal, Annals of Mathematics, decided they were 99 percent certain it was correct, but they couldn’t completely certify the work. Everything they checked was right, but they couldn’t check everything in the colossal proof, especially the volumes of computer calculations.

This outcome wasn’t good enough for Hales, who is launching a 20-year global effort to prove definitively that his proof of the Kepler conjecture is right — and perhaps revolutionize mathematics in the process.

What started as an intellectual diversion became an obsession that has occupied Hales for more than a decade and likely will consume the rest of his career, promising no more glory than professional vindication and a sure place in mathematics history.

Oranges and cannonballs

The question appears simple enough.

How can three-dimensional spheres be packed as tightly as possible so they take up the least amount of space?

This problem arose 400 years ago, when English nobleman Sir Walter Raleigh asked his assistant Thomas Harriot to develop a formula so he could know how many cannonballs were in a stack by looking at its shape.

Harriot took the task a step further and set out to discover the most efficient way to stuff as many cannonballs as possible in the hold of a ship. He asked for advice from one of the foremost mathematicians of the time — German astronomer Johannes Kepler.

Kepler posited the same solution your neighborhood greengrocer might: Oranges (or cannonballs, for that matter) piled in a pyramid allowing each object to sit in the hollows of the layer below it take up less space than if the oranges sit directly atop each other.

For centuries, mathematicians have been searching in vain for absolute proof that this Kepler conjecture is true.

Thomas Callister Hales first learned about the problem in 1982 during a fellowship in England after finishing college at Stanford University. He began to try to solve it as a hobby several years later after earning his doctorate from Princeton.

“I thought, ‘Surely, this can’t be a hard problem to solve; it sounds so easy,’” Hales said. “It was only after I was hooked on the problem that I realized how hard it really was.”

Hales, 49, is a tall, dogged man with thin lips and strong cheekbones who grew up in the heart of Mormon country in Provo, Utah. His father was an ophthalmologist and his grandfather was a physicist at Brigham Young University. Under their influence, Hales grew interested in mathematics and showed early talent for numbers. His mother claims one of his first sentences was “Two 2’s and two 3’s makes 10.”

One reason the Kepler conjecture is so hard to prove is there are more than 5,000 configurations of spheres that must be eliminated to show that the pyramid is best. Another arrangement with each layer of spheres laid out in a honeycomb pattern is equally efficient, but not better.

With the help of computers and a graduate student, Hales began ruling out each of the less-than-perfect configurations.

He first tried a strategy for analyzing the space occupied by the spheres proposed in 1953 by Hungarian mathematician Laszlo Fejes Toth, but the proof grew impossibly complicated. An alternative approach Hales tested also led nowhere.

“There were moments I thought I would still be an old man working on this,” Hales said. “Another big fear was that someone would find an elegant, one-page proof that would undercut all my work.”

Any misgivings dissipated early one morning in November 1994.

While still lying in bed half-asleep, Hales had the key idea that made him realize he could solve the Kepler conjecture: What if he alternated between Toth’s method for studying the space around the spheres and the alternative approach? That way, if he ran into a dead end using one technique, he could shift to the other method and bypass the roadblock.

“As soon as I did a few calculations on the computer, I saw that this would drastically simplify everything,” Hales said. “Once I knew that, I wasn’t willing to give up.”

Hales made the Kepler conjecture his full-time job.

He printed out the 100 candidate sphere arrangements still remaining and hung them on his chalkboard in his office at the time at University of Michigan, tearing down sheets of paper as he eliminated configurations one by one.

He spent months in the engineering library running calculations on as many computers as he could snare, hopping between terminals to keep everything running properly.

“The only true way to get away from the problem was to solve it,” Hales said.

After more than 10 years of work, only two sheets were left on the wall — Kepler’s pyramid arrangement and the equivalent honeycomb pattern.

Hales was dead tired but jubilant.

He had solved the proof.

A proof of the proof

Hales’ achievement established him as a leading mathematician, earning him the 2006 Robbins Prize from the American Mathematical Society and an endowed chair at Pitt.

“What Tom has done is one of the most important mathematical discoveries of the last 25 years,” said Juan Manfredi, chairman of Pitt’s mathematics department.

Hales is modest about his accomplishments, crediting technology instead of his mind.

“There is a lot you can do with a powerful computer that people simply were unable to do 100 years ago,” he said.

Even so, Hales’ reliance on computers also made his proof vulnerable to challenge, since not every calculation in his complex, lengthy code could be validated.

“The news from the referees is bad,” wrote Robert MacPherson, editor of Annals of Mathematics. “They have not been able to certify the correctness of the proof, and will not be able to certify it in the future, because they have run out of energy to devote to the problem.”

The journal conceded to publish Hales’ paper in 2005, but changed its policy on computer proof — it no longer will attempt to verify work done by machines.

Yet the source of doubt also might be part of the solution.

Hales came to Pittsburgh from Ann Arbor in 2001, attracted by the growing community of researchers at Pitt and Carnegie Mellon University working in the field of automated reasoning — building computer systems that can make inferences on their own.

This includes software packages called “proof assistants” designed to check theorems by going through every step of an argument and making sure they follow from mathematical axioms.

“Mathematics for the most part does OK, but proofs are getting more and more complicated and some rely on extensive computation.So it is becoming increasingly important to verify their correctness,” said Jeremy Avigad, a professor of philosophy at CMU.

In 2004, Avigad used a proof assistant to verify the Prime Number Theorem, which describes the probability that a randomly chosen number is prime. A few months later, Microsoft researcher Georges Gonthier used similar software to verify the proof of the Four-Color Theorem, which states that any map needs only four colors to ensure adjacent regions are shaded differently.

On a larger scale, Hales launched the Flyspeck Project — an acronym for “The Formal Proof of Kepler” — that is being paid for by the National Science Foundation. Appropriately, the term “flyspeck” also means to examine closely, or in minute detail.

In the interest of efficiency, traditional pencil-and-paper proofs omit routine logical steps and rely on a mathematician’s intuition to fill in the blanks. In a formal mathematical proof, all the intermediate steps are supplied and checked by a computer, and no appeal is made to intuition.

Using a proof assistant developed by Intel, Hales plans to check every computer calculation and logical step in his proof of the Kepler conjecture to put to rest any lingering uncertainties. He expects this formal proof to take a large, dedicated team of mathematicians across the world at least 20 years of cumulative effort to complete.

If he is successful, it would show that computers can be used to reason in mathematics — not just as glorified calculators to crunch numbers, Avigad said.

“What Tom is doing is questioning some of the very foundations of mathematics and what knowledge means,” Manfredi said. “His work goes to the heart of the scientific method.”

If Hales can use computers to check his exceptionally difficult, 300-page proof of the Kepler conjecture, then theoretically it would be possible to verify almost any mathematical results.

“That would really change the mathematical landscape,” Hales said.

Mathematics always will be a fundamentally creative and human process, but being able to use computers to prove what people can only intuit would bring us closer to truth, Avigad said.

Moreover, the impact of Flyspeck might not be confined to the realm of abstract math. After all, why does proof matter, if we intuitively know the truth anyway?

One answer is that the same technology being used to check the Kepler proof also could make sure that the computers controlling our airplanes, nuclear warheads and stock exchange are working correctly. Likewise, proof assistant software might have detected a bug in an early version of Intel’s Pentium processor that cost the microchip giant $500 million.

“This goes from being something that initially was very theoretical to something where the practical applications are potentially enormous,” Manfredi said.

Hales left Pittsburgh in May for a year-long sabbatical that will take him to Germany, France, Iceland, Vietnam and the Netherlands to build support for the Flyspeck project.

The long journey to prove his proof is just beginning, but this time he is prepared for the challenge ahead, armed with a deeper understanding of how math evolves.

“I think many people think there are these mathematical laws discovered by the Greeks and that was the end of it,” Hales said. “In fact, mathematics is under continual and rapid development, and I was able to see how that works in practice through the proof of the Kepler conjecture.”

If Hales reaches the finish line of his next marathon, his quest for proof will not end there.

“I have a whole drawer full of unsolved problems,” he said. “If I weren’t working on the Kepler conjecture, I would close my eyes, reach in and pull out something else to do.”