By Will Knight 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. But now Georges Gonthier, at Microsoft’s research laboratory in Cambridge, UK, and Benjamin Werner at INRIA in France have proven the theorem in a way that should remove such concerns. They translated the proof into a language used to represent logical propositions – called Coq – and created logic-checking software to confirm that the steps put forward in the proof make sense. “It is a landmark,” says Randy Pollack, from Edinburgh University in Scotland, who wrote one of the first logic-checking programs using Coq. “Mainly because it is such well known theorem and because there was such a row in 1976.” Pollack says many other computer-assisted proofs could be made more credible using the approach. But he notes that it could take years to adapt very complicated proofs in this way. And he says those which require extremely intensive computation might take far too long to check logically. Gonthier says more mathematicians will be encouraged to use computers if they know they can demonstrate the logic behind their calculations. And he suggests this could eventually change the way many mathematicians think. “I’ve found instances where I’m doing things in a completely different way simply because I’m using a computer,” he told New Scientist. But the research could also have an impact beyond mathematics. Microsoft hopes to develop a similar system for checking the logic used in computer programs, which could pre-empt some unforeseen bugs that cause programs to crash. “The discovery has great implications for the future of computing,” says Andrew Herbert,