The Four Colour Theorem: The first time machines mogged mathematicians
Summary
The article recounts the 1976 computer-assisted proof of the Four Color Theorem, highlighting how a machine did heavy lifting and sparked debate about machine-driven proofs. It covers the reception among mathematicians, the credibility of computer-aided proofs, and philosophical questions about proof verification.