Computer proof

⇄ A proof no human can check by hand is still a proof, and the four-colour theorem is known

In 1976 Kenneth Appel and Wolfgang Haken announced a proof that every map can be coloured with four colours so that no two neighbouring regions share one. The proof reduced the problem to almost two thousand configurations and used a computer to…