The Four Colour Theorem: The first time machines mogged mathematicians
This article explores the historical controversy surrounding the 1976 proof of the Four Color Theorem, which was the first major mathematical proof to rely heavily on computer computation. It highlights the tension between traditional mathematicians who valued human-verifiable logic and the emerging reality of computer-assisted discovery.
Why it matters
It marks a pivotal moment in the philosophy of science, questioning the validity of proofs that are too complex for human verification and setting the stage for modern debates on AI-driven research.
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.
Pessimists Archive Newsletter is a reader-supported publication. To receive new posts and support my work, consider becoming a free or paid subscriber.
Get smarter about the news
Sign up free for a feed built around what you actually care about, Dive Deeper research on any story, and the full text of every article.
Create free accountAlready have an account? Sign in