The Four Color Theorem: Early Computer-Assisted Proof Challenged Mathematical Norms

The Four Color Theorem Solved by Computer

In July 1976, mathematicians Kenneth Appel and Wolfgang Haken announced a solution to the Four Color Theorem, a problem that had remained unsolved for over a century. The theorem states that any map can be colored with no more than four colors such that no two adjacent regions share the same color. Their method involved extensive use of a computer, which performed 1,200 hours of computation and made 10 billion decisions to complete the proof.

A New Era of Man-Machine Mathematics

Appel and Haken acknowledged the computer's crucial role, noting that the system "began to teach us things about how to proceed that we never expected" and had "surpassed its creators" in certain intellectual tasks. This marked a departure from traditional human-centric mathematical proof, introducing a new paradigm of man-machine collaboration in mathematics.

Mixed Reception from the Mathematical Community

The mathematical community's reaction was varied, ranging from acceptance to outright rejection. Some mathematicians, like Herbert Wilf, expressed strong disapproval of the method. Others, including Paul Halmos and Frank Bonsall, argued that a proof relying on computer verification of special cases did not constitute proper mathematical science or reasoning. Daniel Cohen stated that admitting such "computer shenanigans" would leave mathematicians "intellectually unfulfilled."

George Spencer-Brown went further, claiming that no proof was actually published and that the situation was akin to "The King's New Clothes." One department head reportedly refused to let Appel and Haken meet his graduate students, believing their method would discourage the search for more elegant, verifiable human proofs.

Impact on Mathematical Proof Standards

The computer-assisted proof of the Four Color Theorem raised fundamental questions about the nature of mathematical proof and verifiability. It challenged the traditional reliance on human-comprehensible reasoning and introduced the concept of proofs too vast for any single human to check. This event highlighted a tension between computational power and established mathematical philosophy.