||Grocers have known for years that the easiest way to stack round items is in a pyramid shape. It took Pitt mathematician Tom Hales 10 years to prove why.
The man boards the train. It's Sunday, and the passenger car is almost empty. The University of Michigan mathematics professor is going home to Ann Arbor after spending the weekend in Chicago. As Tom Hales settles into a seat on the train, he starts working on a geometry riddle that has occupied his free time for several years. He begins by drawing triangles. A stack of drawings piles up by the end of the five-hour trip. A thought occurs to him: There has to be a faster way to generate the shapes. Why not use a computer?
That thought sparked what is perhaps the most ambitious and difficult effort ever to use a computer to solve a math puzzle. The effort would be little more than water cooler chatter among math geeks if Hales' work didn't have the potential of affecting a remarkable variety of things, from credit-card and online banking security to even how war is waged.
What occupied Hales, the Andrew Mellon Professor of Mathematics at the University of Pittsburgh, on that train in the winter of 1994 was a puzzle that had stumped mathematicians for nearly 400 years. The problem is called Kepler's Conjecture. German astronomer and mathematician Johannes Kepler theorized in 1611 that the most efficient way to stack round things is by mounding them, pyramid shape, much like oranges and apples in the produce aisle. The pyramid works best because round things nestle into voids created by the layer below, putting more space to use than if the objects were stacked atop each other. Grocers worldwide have known the superiority of this stacking method for centuries, if only intuitively.
Haleswho credits his physics-teacher grandfather for spurring an early fascination with mathematicsoffers a simple reason for his interest in Kepler: “The problem sounded easy, so I jumped in.” In 1988, he began to solve the riddle in earnest. “I did not have a grand plan to spend 10 years working on the problem,” he admits. “The problem was interesting enough to deserve an afternoon of my time. And the next day I decided to go a little further. Once I got into it, I was trapped.”
His quest to prove Kepler's Conjecture, which took on a new direction after that day on the train, led him to convert his drawings into mathematical symbols. Then, he began reducing the infinite number of stacking arrangements of round objects to just 5,000 possibilities. He did this by eliminating configurations that did not maximize use of space. Density was calculated to find out which arrangement made the best use of space. These calculations can be done in essentially two ways: using pencil and paper or a computer. Hales chose the computer. By using a computer, the 46-year-old Hales made headlines in 1998, 10 years after he began, when he announced that Kepler's stacking theory was true.
Andrzej Trybulec, associate professor at Warsaw University, Bialystok, Poland, and a pioneer in mechanical proof checking, calls Hales' proof “without doubt, one of the most important achievements of the 20th century.”
Hales also received the Chauvenet Prize from the Mathematical Association of America last year; the prize has been awarded since 1925 to some of the world's most distinguished mathematicians. That might have been the end of the story if it weren't for a certain footnote that accompanied the review of his paper.
Hales' proofthe data supporting the reasons why a pyramid shape is bestincluded 40,000 lines of computer code. This code was summarized in a manuscript nearly 300 pages long that was submitted in 1998 for publication in the Annals of Mathematics, perhaps the most prestigious journal of its kind. Scholarly journals generally assign a “referee” or two to check the accuracy of papers before publication. The complexity of Hales' proof warranted a closer look: A dozen mathematiciansan unheard of number of refereeswere assigned to check Hales' paper. Particular sections became the subject of yearlong academic seminars.
In the end, the researchers concluded they were 99 percent sure that Hales was right, but they couldn't be 100 percent certain. In an e-mail to Hales, Robert D. MacPherson, a mathematician at the Institute for Advanced Study at Princeton University and an Annals of Mathematics editor, wrote:
“The news from the referees is bad, from my perspective. 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 do so. This is not what I hoped for.”
Mathematicians are curious people, people with a passion for certainty. They want to know that a proof, an argument for a given premise, is always true in every case. Mathematicians like elegant answers, too, solutions that are innovative and insightful and practical, with applications beyond the ivory towers of academia. For Hales, the MacPherson footnote made his proof none of these things.
At its core, mathematics is deductive proof, which means that certain things can be inferred from certain beliefs. This progression, from assumption to conclusion through connecting steps, is simple logic, something dating as far back as Aristotle, who many consider the father of logic. But Aristotle didn't have a computer. Mathematics and logic made personal computing possible by translating logic-generated equations into electronic commands. By the early 1960s, a new age of automated deduction was dawning. Today, mathematics has become part of everyday life in some surprising ways:
A young woman slams on her car brakes on a rain-slick road, and the vehicle skids out of control. A computer chip, using a mathematical formula called an algorithm, quickly releases then reapplies braking pressure, ending the slide almost as fast as it began. Another example is a computer, using a mathematical formula, reconstructing radio and magnetic waves being reflected from deep inside a man's body. The reconstructed waves take shape on an MRI screen as images of the man's liver, stomach, and other organs.
Clearly, a lot is riding on the accuracy of the formulas that make modern marvels like antilock brakes and MRIs possible. While thousands of scholarly math papers are published each year, mathematicians admit that some have serious errorsone in every 20 papers, according to one estimate. Worse, some mistakes aren't discovered for years.
Take Kepler's Conjecture. It was “proven” by Wu-Yi Hsiang from the University of California at Berkeley in 1990. The findings were trumpeted in 1991 by the highly respected journal Science. Encyclopedia Britannica heralded Hsiang's proof as the “mathematical event of 1991.” The staid American Mathematical Society asked Hsiang in 1993 to lecture on his work, the same year he published what he called an outline of his proof. The problem, according to experts, was that Hsiang was wrong.
After reading Hsiang's proof, Hales threw the article across his office in frustration. The mistakes were readily apparent, he says.
“One of the most unsettling aspects of his article is his deliberate and persistent use of methods that are known to be defective,” Hales wrote about Hsiang in 1994 in The Mathematical Intelligencer. “Mathematicians can easily spot the difference between hand-waving and proof.”
Other mathematicians have chosen simply to ignore Hsiang's work. “Hsiang has not such a good track record,” Frank Quinn, a mathematics professor at Virginia Tech, told The New York Times in April. “I don't want to spend time proving it's wrong.”
This dust-up would mean little outside academia if logic and mathematics weren't at the very heart of the computer. Computer programs are increasingly applying logic and mathematics in innovative ways to a wide array of fields, including medicine, where researchers already envision software being capable of much more than functions like creating images on an MRI screen. Computers may one day have the capability to diagnose diseases. It's precisely that kind of reliance on computers that has philosophers like Carnegie Mellon University's Jeremy Avigad worried. He cautions about our increasing reliance on machines.
“The greater the use of the computer, the more we need to know that it's doing the right thing,” says Avigad, an associate professor of philosophy, whose specialties include mathematical logic and proof theory. “How do you know the computer didn't make a mistake? How do you know the programmer didn't make a mistake? The computer is the problem, and it's the solution.”
Examples abound of problem computers. Consider these: In October 1960, military officials at the North American Air Defense Command were alerted to a missile attack on the United States. What the radar had in fact detected were echoes of the moon rising over Norway.
Six minutes before the first moon landing in July 1969, a computerized guidance system aboard the Apollo 11 Lunar Module bonked. The computer began guiding the spacecraft down in an area covered with dangerously large boulders. A mere 400 feet above the moon's surface, astronaut Neil Armstrong steered the craft to a safer spotlanding with a scant 24 seconds of fuel left.
And in November 1994, a mathematician doing prime number calculations uncovered an embarrassing problem with what was then Intel's newest Pentium processor. The mistake wound up costing the chipmaker $475 million to fix. In each caseand others too numerous to countautomated checking of the mathematical proofs guiding these computers may have uncovered glitches before real headaches surfaced.
Despite all the apparent advantages, machine checking of mathematical formulas that run computers and design questions has been slow to catch on. “There are still many people who resist the automated proof,” says Larry Wos, senior mathematician in the Mathematics and Computer Science Division at Argonne National Laboratory in Chicago. “People want to think they're superiorand they are!” Wos, who is considered a pioneer in automated reasoning, says machines will never totally replace human reasoning, as Armstrong's moon-landing experience shows. Nevertheless, Wos, Hales, and others agree that the need for automated verification is growing as computers increase in complexity. In fact, Hales, hoping to spare future mathematicians the ordeal he went through, has turned to automated verification to prove his proof.
The proof of Kepler's Conjecture is among the most complicated ever, says Hales. He is determined to show it's 100 percent correct. In January 2003, he put together what he calls the Flyspeck Project, a proof of the proof, which is using computer software to recheck every single line of the Kepler proof. Flyspeck, a loose acronym for the Formal Proof of Kepler, is also checking every math theorem cited in the proof, starting with one first published in the late 1800s. Without assistance, Hales estimates it would take 20 years to complete the project, but he expects to reduce that time by recruiting others to help. Hales estimates that the proof of the proof could be finished in five years.
“Tom is really carrying out the verification of his own proof,” says Peter Andrews, professor of mathematics at Carnegie Mellon and a pioneer in the field of automated deduction. “Nothing on this scale of difficulty has previously been attempted.”
Hales sees no other way. “How else do I convince someone there are no mistakes in what I have done?” The Annals of Mathematics is already a believer. Hales' proof is scheduled for publication with a policy announcement about how computer proofs now will be treated.
His ambitious approach puts him in the “forefront of what will indeed be happening in science and mathematics,” says John M. Chadam, professor and chair of Pitt's math department. Marrying mathematics and computers is the field's emerging paradigm, he says. Carnegie Mellon's Avigad calls Hales a “top-rate mathematician,” adding that his work is “breaking new ground.” MacPherson, an Annals editor, told the The New York Times in April that Hales has “made a serious contribution to mathematics.” For Hales, checking the Kepler proof is also a way to quietly champion the emerging age of automated proof-checking
The implications of what's happening on Hales' computer reach far beyond his office. If Flyspeck can verify one of the most complicated mathematical riddles ever, then perhaps software has a bigger role in assuring the safety of everything from commercial flights to bridge design to national defense, all of which rely on mathematical formulas. These formulas are now checked virtually the same way they have been for centurieswith pencil and paper. Flyspeck may change that and, in the process, transform the way mathematics is done for centuries to come.
Kris Mamula is a senior editor of Pitt Magazine.
Links to external Web sites are offered for informational purposes only and the information there is not guaranteed or endorsed by the University of Pittsburgh or its affiliates.