When computers come to the aid of mathematics
01 June 2008
“Mathematics must make a great leap forward”: this is the challenge that Georges Gonthier has set himself.
Georges Gonthier, Senior Researcher, Microsoft Research Cambridge
Since the autumn of 2006, the Microsoft Research Cambridge researcher has been leading the ‘mathematical components' project at the joint research centre set up by Microsoft and the French National Research Institute for Computer Science and Applied Mathematics (INRIA). The 13 researchers working on the project are tackling the thorny problem of computer proof, which proves that a mathematical demonstration is thoroughly accurate. A problem that, according to Gonthier, “becomes increasingly difficult as the theorems become more complex.”
To achieve their ends, the research team is developing a computerised representation of mathematical theories. In other words, a detailed description, not only of this theory, but also of the way it is used, that will enable a computer to automatically check the accuracy of the theorems. It's a field where much remains to be done.
“In most cases,” says Gonthier, “when mathematicians describe a theory in an article or a paper, they present a formal description, but they do not explain how to use the theorem.” With this work, Gonthier, a former INRIA researcher, is continuing research that started at the beginning of the new millennium: in 2005, he was the first to demonstrate by computer the Four Colour theorem, which states that regions on a map may be coloured using no more than four colours in such a way that no two adjacent regions are of the same colour. Gonthier's present work takes some inspiration from the unprecedented development of software components, which was made possible by modern computer languages.
The joint Microsoft/INRIA project aims to foster the use of increasingly sophisticated formal mathematics. Ultimately, it will improve the certification of software - with possible applications including air traffic control, radiotherapy and banking. “Today, the construction of proof is done in a rather ‘artisanal' way,” observes Georges Gonthier. “Our aim is to provide proof that the theories used are reliable, rather than assuming this is the case based on the authors' fame or the claims made for the product.”