The four-colour theorem
The four-colour theorem, that every loopless planar graph has a vertex colouring with at most four colours, was proved by Appel and Haken in 1976, using a computer. Here another proof is given, still using a computer, but simpler than the original.
scientific article; zbMATH DE number 1076870