Georges Gonthier joins the SPECFUN team at the Inria Saclay - Île-de-France centre
Since his thesis alongside Gérard Berry, professor at the Collège de France, Georges Gonthier has been exploring the field of computer verification of mathematical theorems. After having worked for the Inria Rocquencourt centre, the Microsoft research laboratory in Cambridge and taken part in the creation of the joint Inria - Microsoft-Research laboratory, Georges Gonthier is joining the SPECFUN team at the Inria Saclay – Île-de-France centre in order to continue his research projects and get back together with the teams with which he has been working for several years.
A look back at one of his major findings: the demonstration of the four colours theorem.
Since the beginning of his career, Georges Gonthier has endeavoured to verify the accuracy of mathematical theorems using computer science. He has embarked upon demonstrations that represent hundreds of pages of reasoning, in particular the four colours theorem with Benjamin Werner, verified in 20005, and more recently the theory of groups.
Selected this year by the French Ministry of National Education, Higher Education and Research as one of the major discoveries highlighted in a work entitled « 25 découvertes pour les 25 ans de la Fête de la science », (25 discoveries to celebrate 25 years of the science fair), the four colours theorem is once again a topic of conversation today.
"I am proud to be part of these 25 major discoveries but I feel a bit small next to some of the others, such as the invention of the Web. It doesn't really have the same impact", Georges Gonthier underlines. "It is a theorem for the general public in that it is easy to understand, but is not really in tune with modern mathematics. It has nonetheless enabled me to get the subject of computer science verification systems across."
This theorem, which stipulates that four colours suffice in order to colour any map without two regions of the same shade touching each other, has marked Georges Gonthier's career.
"In 1979, when I was a young secondary school student, I took part in the Canadian Mathematics Olympiads and won a prize. This was to spend a week studying mathematics at the University of Waterloo. It was an opportunity to get my hands on computers, which wasn't as common as it is now. During this week, I discovered computer science, programming and the four colours theorem, as Waterloo was a major combinatorial research centre. Many mathematicians were specialists in this subject," Georges Gonthier explains.
In some ways this theorem is behind Georges Gonthier's scientific vocation, and in around 2000 he decided to focus on the problem again: "The proof developed on the subject in 1976 had aged somewhat and had been updated and simplified in 1995. This made it a plausible topic for potential formalisation work." By using the theory of maps, Georges Gonthier and Benjamin Werner solved the problem in 2005.
Today, as part of the SPECFUN, team, Georges Gonthier intends to continue his research work, but also define new objectives. "The work carried out on the theory of groups, for example, has enabled the development of a lot of content in algebra, but unsolved founding principles remain. We are going to carry on with the work and define or invest the resources in order to make progress in research in this field."
These articles could interest you:
- © Photo Bernard Lachaud Computer-assisted proof Mathematical proof by computer science!
- © Inria / Photo Kaksonen Computer-assisted proof A major success for computer-assisted proof
- © Laboratoire commun Inria-Microsoft Research Computer-assisted proof "Our work diagram looked like a Napoleonic war plan!"