La più antica traccia di questo problema si trova in una lettera che nel 1852 il matematico Augustus de Morgan inviò a William Rowan Hamilton, in cui si riporta l'enunciato del teorema come congettura formulta da un suo studente, Frederik Guthrie, diventato poi un fisico.
Da allora sono stati sviluppati molti tentativi di dimostrazione del teorema, che hanno condotto, indirettamente, a molti risultati nell'ambito della teoria dei grafi. Una dimostrazione è stata infine trovata nel 1976 da parte di Kenneth Appel e Wolfgang Haken, due matematici dell'Università dell'Illinois.
L’aspetto più interessante della dimostrazione è il metodo usato. Essa si basa sulla riduzione del numero infinito di mappe possibili a circa 1500 configurazioni per le quali il teorema viene verificato caso per caso dal computer (in circa mille ore complessive, ossia un mese e mezzo). Quando fu presentata la dimostrazione del teorema, il controllo del risultato venne realizzato con un altro programma, implementato su un diverso computer.
Negli anni successivi si sono cercati miglioramenti della dimostrazione: nel 1994 un gruppo di matematici è risucito a "ridurre" la dimostrazione all'analisi di circa 600 configurazioni, che, grazie anche all'evoluzione tecnologica, è stata condotta in poche ore di lavoro da parte di un computer. Per altre informazioni vedi qui.
