Kenneth Appel

THE image of the mathematician, in so far as people have one, has not changed for quite a while. It is Pythagoras drawing in the sand to show that the square on the triangle’s hypotenuse is equal to the sum of the squares on the other two sides. Or it is Newton, in proud seclusion in his Cambridge rooms, proving that an inverse-square law of gravity gives rise to elliptical planetary orbits. These are men who, by the sheer ingenuity of their brains, discovered universal and unchanging truths and expressed them in equations that were poetry by numbers, powerful, elegant and pure.

It fell to Kenneth Appel and Wolfgang Haken, his partner in crime—for that is how many mathematicians saw them—to be the first to disrupt that image, by bringing in computers to help. They proved their particular conjecture, in 1976, partly by using 1,200 hours of time on the IBM 370-168 computer at the University of Illinois, where they both taught mathematics. The mainframe monster made 10 billion logical decisions for them, allowing them to crunch numbers they knew were humanly unfeasible. By using it, though, Dr Appel and his partner changed the nature of mathematics. A purely theoretical science now became also empirical and subject to experiment. Mathematical proof, too, became more uncertain, now that machines were producing reams of results that human intellects could not necessarily see or verify. As one appalled professor declared, “The wolves are in our midst.”

Dr Appel’s conjecture had to do with maps. For more than a century, ever since Francis Guthrie, a maths student, had had a stray thought in 1852, mathematicians had been wondering how many colours it would take to ensure that, no matter how complex a map, no adjacent countries would be the same colour. Guthrie thought the answer was four, but it was just an intuition. He could not prove it mathematically, and nor, for decades, could anyone else. It was a matter of constantly creating new configurations, or maps, and proving that, for them, the four-colour conjecture was true.

By 1925 there were 22 configurations in the set; by 1968 there were 40. The proofs were getting so long that progress was glacial. Even Dr Haken, who had solved the knot problem—finding an algorithm to determine whether a heap of tangled rope could be untangled or had to be cut, the proof of which took three years to write up—announced in 1972 that he was abandoning the map problem. But Dr Appel intervened. Surely computers could do it?

The question was explosive, but his faith in computers was firm. He had written big computer programs for Douglas Aircraft and for the government’s Institute for Defence Analyses, where he had worked on cryptography. To him, computers were partners. When he came to work with the IBM 370-168 he marvelled at its capacity to find “things that weren’t so obvious”. It would “use these bits of knowledge it had in every conceivable way, and any mathematician would say, ‘No, no, no…you have got to do it that way’, but the computer wasn’t doing that.” It was all the more successful, he said, because it was thinking “not like a mathematician”.

Even with its patient, tireless help (harnessed by a “rather effective” program written by one of Dr Appel’s doctoral students, John Koch), the four-colour conjecture was an immense labour to prove. Like Guthrie in the beginning, Dr Appel felt instinctively that it was true. But proving it was like being a hunter in “a moderately thick forest”: “You know very well that if you shoot a gun in any direction it’s eventually going to hit a tree…but yet you haven’t got enough of a description of a forest to formally prove there is a tree there.”

Both he and Dr Haken hugely exceeded their time-allocation on the computer, which belonged to the university administration department. In the end they produced an “unavoidable set” of 1,936 different configurations. Their proof depended on both hand-checking by family members and then brute-force computer power; the result was published over 140 pages in the Illinois Journal of Mathematics and 400 pages of further diagrams on microfiche. They also, in the old-fashioned way, chalked the message on a blackboard in the mathematics department: “FOUR COLORS SUFFICE”.

Aristotle v Galileo

Whether their automated proof sufficed was another question. Many mathematicians furiously attacked them for besmirching the discipline. Dr Appel, whose job and life’s love was to challenge young brains to solve problems without computers, laughed off this reaction. Science was enhanced, not damaged, if theories could be proved in practice. Aristotle’s theorised laws on the free fall of bodies, after all, contained errors that were not corrected until Galileo had carried out experiments.

His proof of the four-colour theorem, he admitted, was not elegant. No new fields of mathematical discovery opened out from it. It was not even of practical use to cartographers. But in harnessing computers as partners and tools, it made a point. From their help came a “wonderful tolerance” in the theorem, a “wonderful robustness”: for him, the same sense of amazement and satisfaction Pythagoras must have felt, and Newton too.