We will discuss the substantial mathematical, computational, historical and philosophical aspects of this celebrated and controversial theorem. Much of this talk should be accessible to undergraduates, but we will also discuss some of the crucial details of the actual revision by Robertson, Sanders, Seymour and Thomas of the original Appel-Haken computer proof. We will additionally cover recent new computer proofs by Gonthier, and by Steinberger, and also the generalisations of the theorem by Hajos and Hadwiger which are currently still open. New software developed by the speaker will be used to visually illustrate many of the subtle points involved, and we will examine the air of controversy that still surrounds existing computer proofs. Finally, the prospect of a human proof will be canvassed.