Mathematicians have employed logic-checking software to help develop a proof of the Four Color Theorem. The method could be used 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 Four Color Theorem states that any four colors are the minimum needed to fill in a flat map without any two regions of the same color touching.

“The discovery has great implications for the future of computing,” says Andrew Herbert, managing director at Microsoft Research Cambridge. “Advances we make into self-checking software have the potential be incorporated into software development tools to make computing in general more reliable and trustworthy.”