Computer generates verifiable mathematics proof

A computer-assisted proof of a 150-year-old mathematical conjecture can at last be checked by human mathematicians. The Four Colour Theorem, proposed by Francis Guthrie in 1852, states that any four colours are the minimum needed to fill in a flat map without any two regions of the same colour touching. A proof of the theorem was announced by two US mathematicians, Kenneth Appel and Wolfgang Haken, in 1976. But a crucial portion of their work involved checking many thousands of maps – a task that can only feasibly be done using a computer. So a long-standing concern has been that some hidden flaw in the computer code they used might undermine the overall logic of the proof.