Computing the burden of proof
THE year: 1611. The person: Johannes Kepler, mathematician and astrologer. The problem: Kepler wanted to give his sponsor, John Matthew Wacker, a new year’s present, but was short of cash. The solution: he wrote a book dedicated to Wacker. The work, Strena Seu de Nive Sexangula (On the Six-Cornered Snowflake), debated the tendency of snowflakes to form beautiful shapes with roughly sixfold symmetry.
We now know that these shapes result from crystal growth in the varying temperature and humidity of storm clouds. A snowflake builds itself particle by particle. At first the structure resembles a microscopic honeycomb. The snowflake retains its hexagonal symmetry as more particles attach themselves to this initial seed. But conditions in storm clouds fluctuate, leading to an endless variety of snowflake shapes.
In the 17th century, the atomic structure of matter belonged to the realm of philosophical speculation. Kepler deduced — in a few pages and without experimental evidence — that a snowflake must be made from many identical tiny spherical units, closely packed together.
The densest way to pack identical spheres is in a honeycomb — consider snooker balls at the start of a frame. Kepler put forward that the most efficient way to pack spheres into a three-dimensional space was similar to the way in which greengrocers stack oranges.
This may seem obvious, but it took nearly 400 years for someone to put together a logical proof that Kepler was right.
In 1998 Thomas Hales announced such a proof, but it involved a 3GB computer file.
What made the proof so complicated? It took a lot of work to rule out vast numbers of irregular packings — showing that these are not as dense as those which greengrocers use.
The wonder is that the question can be reduced to a computation at all. It is no surprise that the answer is gigantic.
Proofs like Hales’s raise a serious philosophical question. Until recently, mathematical proofs could be verified by a competent human being. It may have taken weeks to work through a proof, but it could be done.
Computers have changed the game. They can perform more calculations in a few seconds than the unaided human can in a lifetime. This does not make mathematicians obsolete — the problem still needs to be turned into something that a computer can answer. This is often as difficult and creative as a traditional proof.
Can something be considered a proof if no human can verify it without a computer? For that matter, what is a proof? And why are proofs needed at all?
The traditional model has its roots in the writings of Euclid of Alexandria, particularly his famous Elements. For Euclid, it was not enough to provide circumstantial evidence or numerous examples for mathematical statements. Everything had to be proved, with logic. A familiar example is Pythagoras’s theorem: the square on the longest side of a right-angled triangle is the sum of the squares on the other two sides. This is proposition 47 of Book I of the Elements, and its proof relies on most of the previous 46.
Euclid’s successors made proof the cornerstone of mathematics.
How do we guarantee that an alleged proof has no logical errors or gaps? The time-honoured method is to write it down, so that anyone can check the logic for themselves. The formal definition of proof places no limit on the number of logical steps involved, but there used to be a tacit assumption that the verification process could, and should, be carried out by one unaided human brain.
A 3GB computer file is equivalent to about 10000 full-length novels. It would take about 30 years just to read it. Making sense of it, and checking each deduction, would take several lifetimes. If computers were infallible, we might be happy to accept the results without question. We would only need to check that the computer was obeying the correct instructions, and satisfy ourselves as to the logical structure of the computation.
Unfortunately, computers can make mistakes. The most famous example is a design flaw in the Pentium chip, discovered in 1994. It sometimes got division sums wrong. In practice, such flaws seldom cause serious problems, either because they have no effect or because they lead to such egregious nonsense that it stands out like a sore thumb.
Can a computer-aided proof ever be as trustworthy as traditional proofs, though?
Perhaps not, but humans are far more likely to make undetected errors than computers. If the same program is run on several computers using different operating systems and the results agree, then computer errors are unlikely to have affected the result. Moreover, the problem of size is not confined to computer-aided proofs. One of the big breakthroughs of the late 20th century was a complete list of all possible “finite simple groups" — the basic building blocks of symmetry. The proof — the joint effort of hundreds of mathematicians — occupies about 15000 pages. Can anyone truly read through that and swear that every single step is right?
One school of thought considers these problems to be insurmountable.
Writing in Scientific American in 1993, John Horgan boldly declared the “death of proof". Andrew Wiles’s magnificent proof of Fermat’s last theorem, obtained a few months earlier without computers, was mentioned under the heading, “A splendid anachronism?" Logical proofs, Horgan suggested, might become obsolete — to be replaced by experiments. To prove Pythagoras’s theorem, draw a lot of triangles. To prove the Kepler conjecture, play with oranges. However, rejecting a computer- assisted proof because it might have logical gaps only to replace it with experiments that certainly have gaps makes no sense. Indeed, there are plenty of cases where experimental evidence points to one conclusion while a proof points to a different one.
Most mathematicians rejected Horgan’s article as a selective presentation of a complicated issue. More than a decade later, proof is thriving. But there is nevertheless a fundamental tension between the philosophical definition of a proof — what mathematicians should do — and what they actually do. Mathematicians are much more interested in solving problems than in philosophising about their methods. They set very high logical standards, but they are also pragmatic. Life is too short to write proofs the way philosophers say we should, and the results would be incomprehensible if we did. It took Bertrand Russell and Alfred North Whitehead several hundred pages to give a for
mal proof, in their Principia Mathematica, that 2+2>4. The proof is virtually unreadable, and Russell nearly had a nervous breakdown checking it. So the formal definition of proof may be neat and tidy, but it has several defects. It focuses solely on content and ignores context, it fails to distinguish important ideas from trivial ones, and it does not represent what people do in practice.
Suppose you ask for directions to a small village in Devon. What you don’t want is a lengthy description of how to get your car out of the garage, reverse into your home street and avoid next door’s cat. A list of 10000 instructions, presented as if they were all equally important, is useless.
A more useful set of instructions, then, would be something like this: “Get on the M5 going south until you get past Bristol. Take exit 27 on to the A361 heading for Tiverton."
When you get close to your destination you really do want the details: “Drive along Old Barn Lane, past the duck pond; then take the first right by the dead oak tree onto the cart track — and watch out for the concrete block filling a pothole."
Real proofs, written and published by real mathematicians for the benefit of other mathematicians, are like that. “By a straightforward generalisation of the Bloggs-Smith theorem … an obvious calculation now shows that …”
An accurate formal description of War and Peace might be “a series of words that follow the rules of grammar”. But what matters about any novel is quite different: it has to tell a story. It is the same for proofs. A proof is a series of logical deductions, but it is more informative to see it as a story — a story told by mathematicians to mathematicians, in a familiar language. If it contains logical gaps, or errors, the readers can, and eventually will, notice.
What working mathematicians really mean by a proof, then, is both more and less than a formal list of logical steps. It is more, because the steps have a narrative structure and are equipped with signposts; it is less because gaps are deliberately left whenever the corresponding logical steps are routine and can be reconstructed by anyone familiar with the topic.
This style of proof is more acceptable to human thought patterns than a structureless series of tiny steps, all explicitly cross- referenced to sources that justify them. However, there is a pitfall: steps that in prospect look routine, and are therefore omitted, may conceal unexpected difficulties. Few attempted proofs fall down because some explicit step has been carried out illogically, but a lot fall down because “obvious" steps turn out to be wrong.
For example, it may seem obvious that you can’t cut a solid sphere into a finite number of pieces and fit the same pieces back together to make two solid spheres — each the same size and shape as the original. Obviously the total volume of the pieces can’t change if they are rearranged. However, this argument tacitly assumes that the volumes of the pieces can sensibly be defined.
As it happens, sufficiently complicated pieces need not have sensible volumes at all — and the “impossible" dissection can actually be achieved.
Mathematicians are aware of the danger of omitting allegedly obvious steps, but because the formal style of proof is incomprehensible, they prefer to follow the narrative line. As a result, there are many styles of proof. There is the short, snappy proof, like a poem. There is the proof that carefully assembles key facts, one at a time, and puts them together, like a magazine feature article. There is the 300-page blockbuster that develops entire new theories, and uses them to demolish a major problem — roughly like a novel. And there is the massive, computer-assisted compilation, akin to a telephone directory.
Here’s a simple “poetic" proof. Remove two diagonally opposed corner squares of a chessboard, then try to cover all the remaining squares using 31 “dominoes", each the same size and shape as two adjacent squares. It’s impossible: however you try to make the pieces fit, you always run into trouble. But how do you prove it?
The proof requires one simple idea: every domino must cover one black square and one white square, so the total numbers of each square covered are equal. But the mutilated chessboard has 32 squares of one colour and 30 of the other. Once you get the clever idea of looking at the colours, this proof is short, sweet and convincing.
The novel-like proof is familiar to any professional mathematician; most of us have to work through several of these blockbusters during our careers. Quite a few of us write them. My longest is about 60 pages — a novelette. Wiles’s proof of Fermat’s last theorem is a good example.
Thomas Hales’s proof of the Kepler conjecture is mostly of the phone-directory type, though it sets up the computer calculation with something closer to a poem. That is, there is a simple, very clever idea, which reduces the problem to a very large list of routine computations; this reduction is “poetic". But the poem has no implications until the calculations are carried out, and that bit is a phone book.
Mathematicians prefer poetry to phone books. The famous mathematician Paul Erdös described poetic proofs as from “the Book" — a fanciful image in which God owns a book containing the best proofs, and mere mortals are occasionally afforded a glimpse at it.
In most areas of human activity, accomplishing something difficult is seen as a triumph. It’s the same in mathematics.
Computers open up new realms of discovery, relieving the human brain of routine tasks, leaving it free to concentrate on the big picture. Using computers in proofs — provided it is done carefully — is an intelligent application of technology to extend the powers of the human mind.
And if a long, complicated proof is all we can find, it should be celebrated as a major intellectual achievement, not derided because it’s difficult.
Loading ...