---
title: "The 1st Time Machines Mogged Mathematicians"
slug: the-1st-time-machines-mogged-mathematicians
url: https://listedarticles.com/articles/the-1st-time-machines-mogged-mathematicians
canonical_url: https://newsletter.pessimistsarchive.org/p/the-1st-time-machines-mogged-mathematicians
content_type: essay
language: en
published_at: 2026-10-12T00:00:00.000Z
updated_at: 2026-10-13T23:11:37.683Z
author: "Louis Anslow"
authored_by: human
publisher: "Pessimists Archive Newsletter"
publisher_url: https://newsletter.pessimistsarchive.org/
topics: ["Mathematics", "History", "AI", "Culture"]
license: all-rights-reserved
word_count: 979
reading_minutes: 4
citation: "Louis Anslow, Pessimists Archive Newsletter. \"The 1st Time Machines Mogged Mathematicians.\" 12 Oct 2026. https://newsletter.pessimistsarchive.org/p/the-1st-time-machines-mogged-mathematicians (all-rights-reserved)"
# The full text follows. The web page shows an extract and sends readers
# to the source above; quote the citation and link the canonical URL.
---

# The 1st Time Machines Mogged Mathematicians

> Pessimists Archive's Louis Anslow revisits the 1976 computer-assisted proof of the Four Color Theorem by Appel and Haken, the skepticism and outright rejection it drew from mathematicians, how acceptance slowly came, and the parallels with today's debate over AI-generated mathematics.

In July 1976 a mathematical mystery that confounded mathematicians for more than a century was finally solved: the [Four Color Theorem](https://en.wikipedia.org/wiki/Four_color_theorem)*

***Four Color Theorem** **states:** *no more than four [colors](https://en.wikipedia.org/wiki/Color) are required to color the regions of any [map](<https://en.wikipedia.org/wiki/Map_(graph_theory)>) 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.*

Appel and Haken would later describe how the system *[“began to teach us things about how to proceed that we never expected”](https://celebratio.org/Haken_W/article/793/)*, conceding that the system had *[“surpassed its creators”](https://celebratio.org/Haken_W/article/793/)* 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?*

### **RECEPTION**

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](https://en.wikipedia.org/wiki/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](https://www.exeter.ac.uk/research/groups/education/pmej/pome/pome_8.htm), 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](https://siliconreckoner.substack.com/p/mathematicians-challenged-by-machines), University of Edinburgh 

*“Admitting the computer shenanigans of Appel and Haken to the ranks of mathematics would only leave us intellectually unfulfilled.” -* [Daniel Cohen](https://www.nybooks.com/articles/2003/05/29/a-comedy-of-colors/), 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](https://en.wikipedia.org/wiki/G._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](https://press.princeton.edu/books/paperback/9780691158228/four-colors-suffice?srsltid=AU7gw4U1sVhBN4ZVnjug7bt5Lx4rTaZfyKgkTYWjb_z0oc_zKzX4zlWb))*

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](https://press.princeton.edu/books/paperback/9780691158228/four-colors-suffice?srsltid=AU7gw4U1sVhBN4ZVnjug7bt5Lx4rTaZfyKgkTYWjb_z0oc_zKzX4zlWb))*

### **CREDIBILITY**

The proof would win some high profile endorsements. Legendary mathematician [Bill Tutte](https://en.wikipedia.org/wiki/W._T._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](https://en.wikipedia.org/wiki/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.

### **COVERAGE**

High profile endorsements helped the proof gain credibility and make headlines, with the exception of *[The New York Times](http://nytimes.com)* whose editors *[refused](https://press.princeton.edu/books/paperback/9780691158228/four-colors-suffice?srsltid=AU7gw4U1sVhBN4ZVnjug7bt5Lx4rTaZfyKgkTYWjb_z0oc_zKzX4zlWb)* 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](https://www.ams.org)*.

#### **PHILOSOPHY**

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.

### **WHAT NOW?**

[Robin Wilson](<https://en.wikipedia.org/wiki/Robin_Wilson_(mathematician)>)’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”](https://www.cambridge.org/core/books/abs/petersen-graph/beyond-the-four-colour-theorem/77699F15380E15DD20C63C7564980820)* 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](<https://en.wikipedia.org/wiki/Robin_Wilson_(mathematician)>)’s wonderful recount of this history [here](https://celebratio.org/Appel_KI/article/796/#sender), which seems to be an excerpt from his book [Four Colors Suffice](https://press.princeton.edu/books/paperback/9780691158228/four-colors-suffice?srsltid=AU7gw4U1sVhBN4ZVnjug7bt5Lx4rTaZfyKgkTYWjb_z0oc_zKzX4zlWb)[:](https://press.princeton.edu/books/paperback/9780691158228/four-colors-suffice?srsltid=AU7gw4U1sVhBN4ZVnjug7bt5Lx4rTaZfyKgkTYWjb_z0oc_zKzX4zlWb) *[How the Map Problem Was Solved](https://press.princeton.edu/books/paperback/9780691158228/four-colors-suffice?srsltid=AU7gw4U1sVhBN4ZVnjug7bt5Lx4rTaZfyKgkTYWjb_z0oc_zKzX4zlWb).* It went a long way in helping us recount the history. We’ve reached out to Wilson for an interview.
