|
In Math, Computers Don't Lie. Or Do They?
By KENNETH CHANG New York Times,Published: April 6, 2004 http://www.nytimes.com/2004/04/06/science/06MATH.html A leading mathematics journal has finally accepted that one of the longest-standing problems in the field - the most efficient way to pack oranges - has been conclusively solved. That is, if you believe a computer. The answer is what experts - and grocers - have long suspected: stacked as a pyramid. That allows each layer of oranges to sit lower, in the hollows of the layer below, and take up less space than if the oranges sat directly on top of each other. While that appeared to be the correct answer, no one offered a convincing mathematical proof until 1998 - and even then people were not entirely convinced. For six years, mathematicians have pored over hundreds of pages of a paper by Dr. Thomas C. Hales, a professor of mathematics at the University of Pittsburgh. But Dr. Hales's proof of the problem, known as the Kepler Conjecture, hinges on a complex series of computer calculations, too many and too tedious for mathematicians reviewing his paper to check by hand. Believing it thus, at some level, requires faith that the computer performed the calculations flawlessly, without any programming bugs. For a field that trades in dispassionate logic and supposedly unambiguous truths and falsehoods, that is an uncomfortably gray in- between. Because of the ambiguities, the journal, the prestigious Annals of Mathematics, has decided to publish only the theoretical parts of the proof, which have been checked in the traditional manner. A more specialized journal, Discrete and Computational Geometry, will publish the computer sections. The decision represents a compromise between wholehearted acceptance and rejection of the computer techniques that are becoming more common in mathematics. The debate over computer-assisted proofs is the high-end version of arguments over using calculators in math classes - whether technology spurs greater achievements by speeding rote calculations or deprives people of fundamentals. "I don't like them, because you sort of don't feel you understand what's going on," said Dr. John H. Conway, a math professor at Princeton. But other mathematicians see a major boon: just as the computers of today can beat the grand masters of chess, the computers of tomorrow may be able to discover proofs that have eluded the grandest of mathematicians. The packing problem dates at least to the 1590's, when Sir Walter Raleigh, stocking his ship for an expedition, wondered if there was a quick way to calculate the number of cannonballs in a stack based on its height. His assistant, Thomas Harriot, came up with the requested equation. Years later, Harriot mentioned the problem to Johannes Kepler, the astronomer who had deduced the movement of planets. Kepler concluded that the pyramid was most efficient. (An alternative arrangement, with each layer of spheres laid out in a honeycomb pattern, is equally efficient, but not better.) But Kepler offered no proof. A rigorous proof, a notion first set forth by Euclid around 300 B.C., is a progression of logic, starting from assumptions and arriving at a conclusion. If the chain is correct, the proof is true. If not, it is wrong. But a proof is sometimes a fuzzy concept, subject to whim and personality. Almost no published proof contains every step; there are just too many. The Kepler Conjecture is also not the first proof to rely on computers. In 1976, Dr. Wolfgang Haken and Dr. Kenneth Appel of the University of Illinois used computer calculations in a proof of the four-color theorem, which states that any map needs only four colors to ensure that no adjacent regions are the same color. The work was published - and mathematicians began finding mistakes in it. In each case, Dr. Haken and Dr. Appel quickly fixed the error. But, "To many mathematicians, this left a very bad taste," said Dr. Robert D. MacPherson, an Annals editor., To avoid a repetition, the Annals editors wanted a careful, complete review of Dr. Hales's proof. "But that's not how things turned out," Dr. MacPherson said. "It was a disappointment for all of us." The first group recruited to review the proof spent several years on it, but gave up a year ago, exhausted. Everything checked by the reviewers, led by Dr. Gabor Fejes Toth of the Hungarian Academy of Sciences, turned out to be correct. But the prospect of reviewing every calculation proved too daunting. Dr. MacPherson likened the process to proofreading the listings in a phone book. "Everywhere they looked in the phone book, it was right," he said, "and they looked in a lot of places." The Annals considered publishing the paper with a disclaimer of sorts: This proof has been mostly, but not entirely, checked. Dr. Conway of Princeton, despite his dislike of computer proofs, felt that a disclaimer cast unfair aspersions. "I was very unhappy about it," he said. The proof, Dr. Conway said, included more documentation than usual, including dated records of each step that Dr. Hales and a graduate student, Samuel P. Ferguson, had performed. Faced with such criticism, the Annals editors reconsidered the disclaimer and sent the paper to another mathematician. The new reviewer agreed that the theoretical underpinnings were sound, and the editors arrived at a Solomon-like decision: they split Dr. Hales's paper in two. "The part that's going in The Annals of Mathematics is a proof," Dr. MacPherson said. "We feel he has made a serious contribution to mathematics." In a new policy, The Annals has decided that computer-assisted proofs have merit, but the journal will accord them a lower status than traditional proofs, regarding them more like laboratory experiments that provide supporting evidence. "In some cases, it's not a good idea to verify computer proofs," Dr. MacPherson said. "It took the effort of many mathematicians for many years, and nothing came out of it." Even in traditional proofs, reviewers rarely check every step, instead focusing mostly on the major points. In the end, they either believe the proof or not. "It's like osmosis," said Dr. Akihiro Kanamori, a mathematics professor at Boston University who writes about the history of mathematics. "More and more people say it's a proof and you believe them." That is why an earlier proof of the Kepler Conjecture, first offered eight years before Dr. Hales's, is rarely talked about these days. Dr. Wu-Yi Hsiang of University of California at Berkeley claimed he had a proof in 1990, and in 1993 he published an article that he now calls an outline, not a complete proof. Mathematicians sharply criticized it, saying that it contained holes of logic that they did not think Dr. Hsiang could fill. The level of rigor and detail that mathematicians have demanded of proofs has waxed and waned over the centuries. Major mathematical fields of the 1700's and 1800's like calculus and topology developed without rigorous proofs. "For quite some time in mathematics, arguments were basically descriptive," Dr. Kanamori said. "People would give what we would now call informal arguments." But as mathematicians spun out ever more intuitive arguments, some "proofs" turned out to be false, leading them to shore up the foundations of their earlier work. Mathematicians continue to debate how much rigor a proof requires and whether too much emphasis on details stifles creativity. Dr. Hsiang did not publish his complete proof until 2002, and it appeared as a book rather than in a peer-reviewed journal. Few have bothered to give the book a close read. "Hsiang has not such a good track record," said Dr. Frank Quinn, a mathematics professor at Virginia Tech. "I don't want to spend time proving it's wrong." Dr. Hsiang counters that his proof offers deeper insight and that others' understanding of his techniques is inadequate. Some believe that computers, the source of the debate in Dr. Hales's proof, will actually quiet the debate over proofs. Instead of serving just as a tool for calculations, as in Dr. Hales's proof, computers can also be used to discover new proofs. Mathematicians like Dr. Larry Wos of Argonne National Laboratory use "automated reasoning" computer programs: they enter axioms and the computer sifts through logical possibilities in search of a proof. Because of the huge number of possibilities, a human still needs to tell the computer where to search. "The human mind will never be replaced," Dr. Wos said, butthe advantage of computers is their lack of preconceptions. "They can follow paths that are totally counterintuitive," he said. The software also fills in the tedious work, he said, giving the mathematician more time to contemplate other problems, and it generates as much or as little detail as a mathematician desires. "They are fully rigorous and fully formal in the best sense of the word," Dr. Wos said. "They tell you exactly how each step was obtained." In 1996, Dr. Wos and a colleague, Dr. William McCune, used the software to prove a previously unsolved problem known as the Robbins Conjecture. In a 2003 book, "Automated Reasoning and the Discovery of Missing and Elegant Proofs," Dr. Wos described new proofs and more elegant versions of known proofs discovered by computers. Intel, the microchip giant, uses proof-checking software to check algorithms in its chips, in the hope of avoiding glitches like one in the original 1994 Pentium that caused numbers to divide incorrectly. Dr. Hales has embarked on a similar project called Flyspeck - the letters F, P and K stand for "formal proof of Kepler" - to put to rest any last doubts about the computer proof. Current software, however cannot handle anything nearly as complex as the Kepler Conjecture. Dr. Hales estimates that it will take 20 years of cumulative effort by a team of mathematicians to complete. As for his 1998 proof of the Kepler Conjecture, Dr. Hales said that final publication, after a review process, originally expected to last a few months, would be almost anticlimactic. "For me, the big moment was when I completed the proof," Dr. Hales said. "And I don't think anything will change when I see it in print." Dr. Conway of Princeton, despite his dislike of computer proofs, felt that a disclaimer cast unfair aspersions. "I was very unhappy about it," he said. The proof, Dr. Conway said, included more documentation than usual, including dated records of each step that Dr. Hales and a graduate student, Samuel P. Ferguson, had performed. Faced with such criticism, the Annals editors reconsidered the disclaimer and sent the paper to another mathematician. The new reviewer agreed that the theoretical underpinnings were sound, and the editors arrived at a Solomon-like decision: they split Dr. Hales's paper in two. "The part that's going in The Annals of Mathematics is a proof," Dr. MacPherson said. "We feel he has made a serious contribution to mathematics." In a new policy, The Annals has decided that computer-assisted proofs have merit, but the journal will accord them a lower status than traditional proofs, regarding them more like laboratory experiments that provide supporting evidence. "In some cases, it's not a good idea to verify computer proofs," Dr. MacPherson said. "It took the effort of many mathematicians for many years, and nothing came out of it." Even in traditional proofs, reviewers rarely check every step, instead focusing mostly on the major points. In the end, they either believe the proof or not. "It's like osmosis," said Dr. Akihiro Kanamori, a mathematics professor at Boston University who writes about the history of mathematics. "More and more people say it's a proof and you believe them." That is why an earlier proof of the Kepler Conjecture, first offered eight years before Dr. Hales's, is rarely talked about these days. Dr. Wu-Yi Hsiang of University of California at Berkeley claimed he had a proof in 1990, and in 1993 he published an article that he now calls an outline, not a complete proof. Mathematicians sharply criticized it, saying that it contained holes of logic that they did not think Dr. Hsiang could fill. The level of rigor and detail that mathematicians have demanded of proofs has waxed and waned over the centuries. Major mathematical fields of the 1700's and 1800's like calculus and topology developed without rigorous proofs. "For quite some time in mathematics, arguments were basically descriptive," Dr. Kanamori said. "People would give what we would now call informal arguments." But as mathematicians spun out ever more intuitive arguments, some "proofs" turned out to be false, leading them to shore up the foundations of their earlier work. Mathematicians continue to debate how much rigor a proof requires and whether too much emphasis on details stifles creativity. Dr. Hsiang did not publish his complete proof until 2002, and it appeared as a book rather than in a peer-reviewed journal. Few have bothered to give the book a close read. "Hsiang has not such a good track record," said Dr. Frank Quinn, a mathematics professor at Virginia Tech. "I don't want to spend time proving it's wrong." Dr. Hsiang counters that his proof offers deeper insight and that others' understanding of his techniques is inadequate. Some believe that computers, the source of the debate in Dr. Hales's proof, will actually quiet the debate over proofs. Instead of serving just as a tool for calculations, as in Dr. Hales's proof, computers can also be used to discover new proofs. Mathematicians like Dr. Larry Wos of Argonne National Laboratory use "automated reasoning" computer programs: they enter axioms and the computer sifts through logical possibilities in search of a proof. Because of the huge number of possibilities, a human still needs to tell the computer where to search. "The human mind will never be replaced," Dr. Wos said, butthe advantage of computers is their lack of preconceptions. "They can follow paths that are totally counterintuitive," he said. The software also fills in the tedious work, he said, giving the mathematician more time to contemplate other problems, and it generates as much or as little detail as a mathematician desires. "They are fully rigorous and fully formal in the best sense of the word," Dr. Wos said. "They tell you exactly how each step was obtained." In 1996, Dr. Wos and a colleague, Dr. William McCune, used the software to prove a previously unsolved problem known as the Robbins Conjecture. In a 2003 book, "Automated Reasoning and the Discovery of Missing and Elegant Proofs," Dr. Wos described new proofs and more elegant versions of known proofs discovered by computers. Intel, the microchip giant, uses proof-checking software to check algorithms in its chips, in the hope of avoiding glitches like one in the original 1994 Pentium that caused numbers to divide incorrectly. Dr. Hales has embarked on a similar project called Flyspeck - the letters F, P and K stand for "formal proof of Kepler" - to put to rest any last doubts about the computer proof. Current software, however cannot handle anything nearly as complex as the Kepler Conjecture. Dr. Hales estimates that it will take 20 years of cumulative effort by a team of mathematicians to complete. As for his 1998 proof of the Kepler Conjecture, Dr. Hales said that final publication, after a review process, originally expected to last a few months, would be almost anticlimactic. "For me, the big moment was when I completed the proof," Dr. Hales said. "And I don't think anything will change when I see it in print." Dr. Conway of Princeton, despite his dislike of computer proofs, felt that a disclaimer cast unfair aspersions. "I was very unhappy about it," he said. The proof, Dr. Conway said, included more documentation than usual, including dated records of each step that Dr. Hales and a graduate student, Samuel P. Ferguson, had performed. Faced with such criticism, the Annals editors reconsidered the disclaimer and sent the paper to another mathematician. The new reviewer agreed that the theoretical underpinnings were sound, and the editors arrived at a Solomon-like decision: they split Dr. Hales's paper in two. "The part that's going in The Annals of Mathematics is a proof," Dr. MacPherson said. "We feel he has made a serious contribution to mathematics." In a new policy, The Annals has decided that computer-assisted proofs have merit, but the journal will accord them a lower status than traditional proofs, regarding them more like laboratory experiments that provide supporting evidence. "In some cases, it's not a good idea to verify computer proofs," Dr. MacPherson said. "It took the effort of many mathematicians for many years, and nothing came out of it." Even in traditional proofs, reviewers rarely check every step, instead focusing mostly on the major points. In the end, they either believe the proof or not. "It's like osmosis," said Dr. Akihiro Kanamori, a mathematics professor at Boston University who writes about the history of mathematics. "More and more people say it's a proof and you believe them." That is why an earlier proof of the Kepler Conjecture, first offered eight years before Dr. Hales's, is rarely talked about these days. Dr. Wu-Yi Hsiang of University of California at Berkeley claimed he had a proof in 1990, and in 1993 he published an article that he now calls an outline, not a complete proof. Mathematicians sharply criticized it, saying that it contained holes of logic that they did not think Dr. Hsiang could fill. The level of rigor and detail that mathematicians have demanded of proofs has waxed and waned over the centuries. Major mathematical fields of the 1700's and 1800's like calculus and topology developed without rigorous proofs. "For quite some time in mathematics, arguments were basically descriptive," Dr. Kanamori said. "People would give what we would now call informal arguments." But as mathematicians spun out ever more intuitive arguments, some "proofs" turned out to be false, leading them to shore up the foundations of their earlier work. Mathematicians continue to debate how much rigor a proof requires and whether too much emphasis on details stifles creativity. Dr. Hsiang did not publish his complete proof until 2002, and it appeared as a book rather than in a peer-reviewed journal. Few have bothered to give the book a close read. "Hsiang has not such a good track record," said Dr. Frank Quinn, a mathematics professor at Virginia Tech. "I don't want to spend time proving it's wrong." Dr. Hsiang counters that his proof offers deeper insight and that others' understanding of his techniques is inadequate. Some believe that computers, the source of the debate in Dr. Hales's proof, will actually quiet the debate over proofs. Instead of serving just as a tool for calculations, as in Dr. Hales's proof, computers can also be used to discover new proofs. Mathematicians like Dr. Larry Wos of Argonne National Laboratory use "automated reasoning" computer programs: they enter axioms and the computer sifts through logical possibilities in search of a proof. Because of the huge number of possibilities, a human still needs to tell the computer where to search. "The human mind will never be replaced," Dr. Wos said, butthe advantage of computers is their lack of preconceptions. "They can follow paths that are totally counterintuitive," he said. The software also fills in the tedious work, he said, giving the mathematician more time to contemplate other problems, and it generates as much or as little detail as a mathematician desires. "They are fully rigorous and fully formal in the best sense of the word," Dr. Wos said. "They tell you exactly how each step was obtained." In 1996, Dr. Wos and a colleague, Dr. William McCune, used the software to prove a previously unsolved problem known as the Robbins Conjecture. In a 2003 book, "Automated Reasoning and the Discovery of Missing and Elegant Proofs," Dr. Wos described new proofs and more elegant versions of known proofs discovered by computers. Intel, the microchip giant, uses proof-checking software to check algorithms in its chips, in the hope of avoiding glitches like one in the original 1994 Pentium that caused numbers to divide incorrectly. Dr. Hales has embarked on a similar project called Flyspeck - the letters F, P and K stand for "formal proof of Kepler" - to put to rest any last doubts about the computer proof. Current software, however cannot handle anything nearly as complex as the Kepler Conjecture. Dr. Hales estimates that it will take 20 years of cumulative effort by a team of mathematicians to complete. As for his 1998 proof of the Kepler Conjecture, Dr. Hales said that final publication, after a review process, originally expected to last a few months, would be almost anticlimactic. "For me, the big moment was when I completed the proof," Dr. Hales said. "And I don't think anything will change when I see it in print."
|