"Our work diagram looked like a Napoleonic war plan!"
© Laboratoire commun Inria-Microsoft Research
Six years transpired between the start of the project and the end of the proof of the Feit-Thompson theorem, which came on 20 September 2012. Following is the account of this modern-day adventure.
Interview with Georges Gonthier, Microsoft Research-Inria joint laboratory.
What was the project's objective?
The goal was to translate the idea of the mathematical statement into a form that could be understood by the computer so that it could determine whether the proof was correct and complete. Indeed, the proof is the end goal that allows you to test all of the developments that were carried out beforehand and were necessary in order to achieve the proof. This proof draws on numerous fields of mathematics: linear algebra, geometry, number theory, Galois theory, finite fields, etc. We had to develop the mathematical libraries necessary for completing all the stages of the proof.
Consequently, we spent the first three years codifying the simplest mathematics, then one year working on the first half of the proof, which was based on this type of mathematics. It took another year to develop the tools for another branch of the mathematics, then one final year for the second part of the proof.
How was the work organised during those six years?
Around ten researchers and post-doctoral students contributed to the work to different degrees and over different periods of time. As a coordinator, I was working full-time on the problem. The work had to be divided up because of the geographical dispersal of the participants in Cambridge, Inria Saclay and Inria Sophia Antipolis. However, several researchers were able to work on the same problem at a given site. For the last part of the proof on 20 September, everyone mucked in!
Did you expect the work to take so long?
I'd already gained experience in proving the four colour theorem. I knew that it took a long time to put the fundamentals in place before the work could actually move forward: you need to understand how to build the libraries before working on them and testing them with this proof, which is the end goal. I expected the whole project to take five to six years, so there weren't any surprises in that respect! But it was different for my colleagues. Six years ago when I sketched out a diagram representing all of the sections to be developed and how they were interconnected, my audience thought it looked like a Napoleonic war plan! On 20 September I received a photo of myself wearing a bicorn hat!
Were there any surprises during the work?
We certainly had a few surprises, particularly in terms of how to write the libraries so that we could assemble them flexibly. It was a fundamental problem that we approached by using the same principle as for creating the software components, which can be easily connected with one other: by adding a section of code stating how to combine with other software. It was then that I discovered we could use the same mechanism as for interpreting mathematical annotations and that Coq had the necessary tools.
We also identified a few inconsequential transcription errors in the proof thanks to the programme.
What is the impact of this work?
The fact that we've managed to treat a notoriously difficult problem using a computer shows that there's been progress in the quality of the tools and techniques employed in this mathematical codification work. It's still too early to judge the impact of this proof. However, our results have been made available as they were produced and the libraries developed have already been picked up: today, a large number of publications use Coq and our library. We now need to focus on distributing our results, which was somewhat sidelined during those years.
Is there a follow-up to this work planned?
We now need to learn the lessons of this experience to prepare the tools for what comes next and take the time to reflect. With word having got out, we've already received suggestions for problems. The natural next step would be the complete classification theorem, but that's an undertaking that far exceeds the joint laboratory's human resources. The entire world's mathematics labs would need to get involved! I've also got a few of my own ideas, but nothing's been decided yet.