Mathematical evidence, too complex ever to be fully checked by a human, is now accepted as valid, writes Keith Devlin
What exactly is a mathematical proof? This thorny question was raised again last month when an American mathematician announced a solution to a 400-year-old problem posed by the astronomer Johannes Kepler.
Thomas Hales of the University of Michigan claimed that he had proved correct a guess Kepler made in 1611.
Hales posted his entire proof on the Internet for anyone to check. However, it involves 250 pages of text and about three gigabytes of computer programs and data. To follow Hales’s argument, you have to download and run his programs.
As Hales admits, with a proof this complex, it will be some time before anyone can be sure it is correct. By posting everything on the World Wide Web he has, in effect, challenged the mathematical community to see if they can find anything wrong. If no one can, eventually everyone will agree the proof is correct.
Experts who have visited the website think it looks convincing, but it will require months of painstaking work before mathematicians are willing to put their imprimatur on it.
The situation is reminiscent of the Four Colour Problem solution, published by Kenneth Appel and Wolfgang Haken in 1976. Their proof that four colours are all you need for any map drawn on a plane, so that countries with a common border are coloured differently, also involved a mix of ordinary mathematical reasoning and masses of computation. On that occasion, a few mathematicians remained skeptical about the proof for several years.
Now that we have the Internet, any mathematician has access to Hales’s entire proof and all its computer programs, so a consensus should emerge much more quickly.
But in both cases, the whole question of what constitutes a mathematical proof is raised.
In principle, the matter is straightforward. A proof is a logically valid piece of reasoning that establishes a particular result. This definition works well enough for the kinds of proofs encountered in high school and university mathematics classes.
The situation is very different when it comes to long and complicated arguments, such as Andrew Wiles’s 250- page proof of Fermat’s Last Theorem. Probably 30 mathematicians around the world have read and understood the entire proof since it was published in 1994.
For the rest of us, if we accept that Fermat’s Last Theorem has been proved, the proof that convinces us relies not on logic but on the reputation and record of those who have read it.
In practice, that’s already a shift in what we mean by a ”proof”, although it does involve somebody having checked all the details, so in one sense nothing has changed. But when a complicated proof also requires a computer to perform a calculation that no human could possibly check, we are talking about proofs that no person has ever read in their entirety, and perhaps never will. And that’s something new.
If you have confidence in modern computers, this situation is hardly a cause for alarm. By accepting as valid mathematical proofs that cannot be completely checked by a human, we have crossed a Rubicon as to what constitutes a mathematical proof.
Kepler’s problem involves the most efficient way to pack equal-sized spheres in a large crate. Should you pack them in identical layers, with each sphere sitting right on top of the one beneath? Or can you get more spheres into the box if you stagger the layers, the way greengrocers stack oranges, so that the oranges in each higher layer sit in the hollows formed beneath?
For a small crate, the answer can depend on the dimensions of the crate and the spheres. But for a very large crate, you can demonstrate that the orange-pile arrangement is more efficient.
Kepler believed this to be so but was unable to prove it. Succeeding generations of mathematicians were also unsuccessful.
Though it never achieved the general fame of Fermat’s Last Theorem, Kepler’s sphere-packing conjecture was similar in that while the problem was easy to understand, it seemed fiendishly difficult to solve.
In 1953, Hungarian mathematician Laszlo Toth managed to reduce Kepler’s problem to a huge calculation involving many specific cases.
In 1994, Hales evolved a strategy for solving the problem along the lines Toth had suggested. In August, he proved Kepler’s guess had been correct. While this might have no direct applications, the efficient packing of spheres is a crucial part of the mathematics behind the error-detecting and error-correcting codes used to store information on compact disks and to compress information for efficient transmission around the world.
In today’s information society, you can’t get a more significant application than that.