Four Color Theorem Computer Proof (1976)
Kenneth Appel and Wolfgang Haken at the University of Illinois announced they had proved the four color theorem—that any map can be colored with just four colors so no adjacent regions share a color. Their proof required over 1,000 hours of computer time to verify 1,936 special cases. It was the first major mathematical theorem proved with substantial computer assistance.
The mathematical community reacted with 'equal parts celebration and dismay.' Many mathematicians refused to accept a proof humans couldn't verify by hand. Colleague William Tutte celebrated that they 'smote the kraken' while others despaired at computers 'encroaching on human ingenuity.'
The proof gained grudging acceptance and established computer-assisted proof as legitimate, if controversial. It foreshadowed today's debates about AI-generated proofs and what constitutes mathematical understanding versus mere verification.
The 1976 controversy over computer proofs mirrors today's debates about AI theorem provers. The key difference: modern formal verification in Lean provides stronger guarantees than 1976's case-checking, but questions about mathematical insight versus brute-force verification persist.
