The Four Colour Theorem has been proven using a computer program called Coq v7.3.1. The proof is based on previous work but includes new ideas. The report explains the history of the problem, what was proved, and how the proof was conducted. The researchers used the Coq assistant and a tactic shell to write their proof scripts. The detailed formal proof and the development process are also described. The main goal was to formally prove the Four Colour Theorem, and the key finding is that it has been successfully achieved.