The Four Colour Theorem: The first time machines mogged mathematicians

The Four Colour Theorem was a major milestone in mathematics, solved by Ken Appel and Wolfgang Haken in 1976. They used a computer to prove the theorem, marking the first time machines were used to outperform mathematicians in solving a problem. The theorem states that any planar map can be coloured with four colours such that no two adjacent regions have the same colour. Appel and Haken's proof relied on a computer program that checked over 1,500 cases, taking over 1,200 hours to run. Their work was initially met with skepticism by some mathematicians, but it was later widely accepted as a major breakthrough.