The Four Colour Theorem: The first time machines mogged mathematicians

In 1976 Kenneth Appel and Wolfgang Haken settled the century-old Four Color Theorem by combining traditional reasoning with massive computer work: roughly 1,200 hours of computation and billions of case checks, with programmer John Koch implementing key algorithms. Their computer-aided method produced a proof that the human eye could not fully survey, and the team admitted the system sometimes "taught" them new ways to proceed. The result forced a sharp question onto the mathematical community: can a proof that no single person can verify still be trusted as mathematics? Reactions split sharply along philosophical and generational lines. Some leading figures condemned the method as non-mathematical or intellectually unsatisfying, others accepted it grudgingly or celebrated it, and one department even barred the authors from speaking to students to avoid stifling attempts at more elegant proofs.

The proof gained important endorsements - Bill Tutte, Heinrich Heesch, and others - and eventually mainstream recognition after initial newspaper reluctance. Philosophers and mathematicians continued the debate: Thomas Tymoczko argued that an un-surveyable proof departs from traditional proof, while Ted Swart defended computer-assisted work as an extension of hand calculation and noted human fallibility. The episode marked a watershed in the philosophy and practice of mathematics, illustrating how machines can reshape standards of rigor, trust, and the direction of future research; Robin Wilson’s Four Colors Suffice is cited as a detailed historical account.