In July 1976 a mathematical mystery that confounded mathematicians for more than a century was finally solved: the Four Color Theorem*
*Four Color Theorem states: no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color
Its authors - Kenneth Appel and Wolfgang Haken - would credit an unconventional collaborator: a computer had done much of the mathematical heavy lifting, 1,200 hours of compute and 10 billion decisions to be exact.
Computer Programmer John Koch would help Appel & Haken with algorithmic work.
Appel and Haken would later describe how the system “began to teach us things about how to proceed that we never expected”, conceding that the system had “surpassed its creators” in certain intellectual tasks. A brave new world of man-machine mathematics had begun, begging a question: are we to trust a mathematical proof is too vast for any human to verify?
Reactions from mathematicians ranged from acceptance, to rejection and even denial - rather than universal adoration. Mathematicians - who pride themselves on rationality - were suddenly confronted with a mathematical moloch in what must have felt like irreligious heresy.
“God wouldn’t let the theorem be proved by a method as terrible as that!” - Herbert Wilf, University of Pennsylvania
Some protested a mathematical proof without mathematical reasoning and were vocal about it:
“the present proof relies in effect on an Oracle, and I say down with Oracles! They are not mathematics” … - Paul Halmos, UC Santa Barbara
“if the solution involves computer verification of special cases . . . such a solution does not belong to mathematical science at all.” - Frank Bonsall, University of Edinburgh
“Admitting the computer shenanigans of Appel and Haken to the ranks of mathematics would only leave us intellectually unfulfilled.” - Daniel Cohen, Hunter College NYC
Others refused to believe a proof had even been found at all:
“not only is no proof to be found in what they published, but there is not anything that even begins to look like a proof… …It is the most ridiculous case of ‘The King’s New Clothes’ that has ever disgraced the history of mathematics” - George Spencer-Brown, Cambridge University
One mathematics department head refused to allow Appel and Harken to meet his graduate students, claiming their method removed incentive to find a verifiable and more elegant proof:
“Since the problem had been taken care of by a totally inappropriate means, no first-rate mathematician would now work any more on it, because he would not be the first one to do it, and therefore a decent proof might be delayed indefinitely.” (recounted by Robin Wilson in Four Colors Suffice)
Amusingly - and predictably - age seemed to be the determining factor in receptivity to computer aided proofs. After a presentation by Harken’s son about the proof (which he helped his father with) the audience reportedly split into two groups: “over-40s could not be convinced that a proof by computer was correct, while the under-40s could not be convinced that a proof containing 700 pages of hand calculations could be correct.” (via Robin Wilson’s book Four Colors Suffice)
The proof would win some high profile endorsements. Legendary mathematician Bill Tutte - who once publicly doubted their computer aided method of choice in a journal - would concede it solved, celebrating with a poem:
Wolfgang Haken
Smote the Kraken
One! Two! Three! Four!
Quoth he: “The monster is no more.”
Esteemed German mathematician Heinrich Heesch accepted the proof, begrudgingly - since he had spent four decades working on the problem, and even created the key algorithmic methods applied by Appel and Haken. Other mathematicians treated the proof seriously too, like Ted Swart - who had been closing in on a computer aided proof around the same time - only to be beaten to it.
High profile endorsements helped the proof gain credibility and make headlines, with the exception of The New York Times whose editors refused to cover the breakthrough for fear it was a false alarm. Once it was considered legitimate months later, editors argued it was no longer newsworthy. It only appeared in paper of record thanks to an op-ed by Lipman Bers, President of The American Mathematical Society.
The debate over ‘proof without reasoning’ intensified in 1979, when philosopher Thomas Tymoczko argued in The Journal of Philosophy that an un-surveyable proof was not a traditional mathematical proof (though he didn’t doubt the proof technically proved what it claimed to)
“No mathematician has seen a proof of the 4CT, nor has any seen a proof that it has a proof. Moreover, it is very unlikely that any mathematician will ever see a proof of the 4CT.” - Thomas Tymoczko
Ted Swart would push back on Tymoczko, in a response published in ‘American Mathematical Monthly’, he’d later sum his argument up saying “I regard computer-assisted proof as just an extension of pencil and paper.” Swart would also question the implied infallibility of human mathematicians, quipping “Human beings get tired, and their attention wanders, and they are all too prone to slips of various kinds . . . Computers do not get tired.” His retort would later win an award for expository writing.
Robin Wilson’s book on the history of theorem noted that in 1978 Bill Tutte would confront the question of what the future held for mathematicians in the face of machine made proofs:
His advice? “Be of good cheer. You can continue in the same general line of research” and of course he offered a poem too:
The Four Colour Theorem is the tip of the iceberg,
the thin end of the wedge
and the first cuckoo of Spring.
This, no doubt written by a human being.
We urge you to read Robin Wilson’s wonderful recount of this history here, which seems to be an excerpt from his book Four Colors Suffice: How the Map Problem Was Solved. It went a long way in helping us recount the history. We’ve reached out to Wilson for an interview.
Support Pessimists Archive
It has never been more important to learn from the history of reactions to new ideas and technologies.
Help us increase output through 2026 and into 2027
SMALL SUPPORT: Subscribe
$20/month on Substack (here)
BIG SUPPORT: become a Pessimists Patron
$100/month on X.com (here)
$1,000/year on Substack (here)
PessimistsArchive.org is also open to taking tax deductible contributions via surrogate nonprofits, email for more information.
Instagram Engineering
Shopify Engineering
