By Rob Knies, Managing Editor, Microsoft Research
On Nov. 22, in a Parisian ceremony at the Institut de France, Georges Gonthier, a principal researcher at Microsoft Research Cambridge (opens in new tab), was awarded the 2011 EADS Foundation Grand Prize in Computer Science. The award, established in 2007 by the corporate foundation of the European Aeronautic Defence and Space Co. and presented by France’s Académie des sciences, recognizes the achievement of a scientist in a French laboratory who has made exceptional contributions to the vitality and influence of computer-science research while building outstanding cooperation with industry. Gonthier, who gained acclaim for his 2005 proof of the Four Colour Theorem (opens in new tab), spends a significant part of his time working at the Microsoft Research-INRIA Joint Centre (opens in new tab), collaborating with French researchers from INRIA (opens in new tab), the French National Research Institute for Computer Science and Applied Mathematics. In the days preceding the awards ceremony, he found a few minutes to discuss the recognition and his work:
Q: What does it mean to you to receive acknowledgment such as this?
MICROSOFT RESEARCH PODCAST
AI Frontiers: The future of scale with Ahmed Awadallah and Ashley Llorens
This episode features Senior Principal Research Manager Ahmed H. Awadallah, whose work improving the efficiency of large-scale AI models and efforts to help move advancements in the space from research to practice have put him at the forefront of this new era of AI.
Gonthier: It means a lot, because it signifies cross-disciplinary recognition of my work. I’ve been working on this project on ramping up theorem-proving tools to tackle research-level mathematical work. There are many prominent French mathematicians in the Académie, and rather few computer scientists. Obviously, the fact that they like what I’ve done bodes well for the next tech-transfer phase.
Q: You are actively involved in the Microsoft Research-INRIA Joint Centre. How does that collaboration work, and how do you allocate your time among your various responsibilities?
Georges Gonthier
Gonthier: Back in 2005, a few INRIA colleagues got excited about the work I was planning in the wake of the big four-colour splash and, with the creation of the joint centre, found the means of setting up an effective collaboration. There have since been four to five INRIA researchers working with me on the various aspects of the project and slightly more postdocs, Ph.D.s, and visitors. About half of them are based at the Sophia Antipolis INRIA location, so, with me in Cambridge, there is a lot of interaction through our source repository—though we do try to meet regularly. Last year, we started a wider collaboration with an EU-sponsored project with three other universities, in the Netherlands, Spain, and Sweden.
We each balance our involvement according to our respective research agendas. As leader, I focus most of my time and effort on the project, even when I am in Cambridge. This is the core of my work, but I divide my office presence roughly between 70 to 75 percent in Cambridge and the rest in the joint centre in Orsay—not counting all the time I’m on the road
Q: One of your best-known achievements is your fully checked formal proof of the Four Colour Theorem. How were you able to accomplish this, and what impact has it had on the research community?
Gonthier: It’s hard for me to know, because people do not tell me directly, but I am still asked to give lectures on the topic, and I keep bumping into young researchers who say they are “honored” to meet me, so I guess I must have made a splash.
I got initially hooked on the Four Colour problem back in 2000, when I handed out some of the decision procedures used in the proof as a programming assignment to my students at École Polytechnique. It bothered me that part of the proof, even the revised one, consisted of unverified—and unverifiable—C code. I’d written cleaner versions of the procedures for the assignment solution, and I wondered whether they could actually be formally verified using an interactive computer theorem-proving tool. I tried, and it turned out to be a relatively straightforward exercise, but then I realized I should also prove that the procedures’ technical specifications were correct—that they were consistent with the mathematical proof. That was going to be much harder, because of the limited support for general mathematics.
It became a bit of a spare-time, back-burner activity until the spring of 2004, when I had a breakthrough: a significant simplification in the proof, which the crack team of combinatorists that had revised the proof had missed, but which the detailed computer formalization had uncovered. That’s what ultimately let me finish the job.
That Four Colour Theorem proof provided hard evidence that computer-proof systems could handle nontrivial maths and complex algorithms, and I do hope it has inspired others to pick up theorem-proving tools and boldly try do difficult and interesting things with them. Examples of this certainly appear with increasing regularity.
The observation that good organization of the theories and proofs was instrumental in getting the job done—and that this requires the use of a variety of software-engineering techniques—was the basis of my current project at the joint centre. I’m afraid it got a bit lost in the celebratory noise of the achievement.
Q: What is your current research focus?
Gonthier: My top project goal is to build a computer formalization of a large and complex proof in group theory—the Feit-Thompson proof of the Odd Order Theorem—largely as a motivation for developing a comprehensive library of formalized math. In turn, the main objective of that was to coin the techniques for organizing such a library.
In the first couple of years, I did a lot of the latter, and progress on the main goal was minimal. Even progress on the library was slow at the start, with frequent backtracking. Fortunately, with my experience on the Four Colour Theorem, I’d come to expect that and knew to hang on. Last year, things accelerated suddenly, and we got over half of the main proof done—the part known as “local analysis”—so we must finally have gotten the groundwork right.
The big push now is to finish the whole thing. We seem to be attracting the attention of real, senior mathematicians, so perhaps the Odd Order Theorem will be, for them, the same inspiration as the Four Colour Theorem was for computer scientists.
Q: What challenges lie ahead for your field?
Gonthier: To take these tools to professional mathematicians and change the way mathematics is done. There is also another challenge, closer to home for Microsoft: to adapt the mathematical-abstraction techniques we’ve coined to develop a new generation of program specification and verification tools. I have several colleagues in Microsoft Research working on this very topic, and after my foray into blue-sky research, I will try to join forces with them. That was part of the plan when I embarked on this.
Q: Who inspires you?
Gonthier: Three people spring to mind. One is Robin Milner, who created most of the computer-science theories with which I’ve worked, including the design of the Logic for Computable Functions system, of which the Coq (opens in new tab) system I use is a descendant. I’m especially in awe of his knack for simplifying a theory to its bare essentials.
Another is Gilles Kahn, because he always took the view that formalisms ought to be tested by building and using computer tools. He could do brilliant theory, as well, but what really excited him was to tinker with stuff. He was one of the earliest external Coq adopters.
And then there’s John H. Conway. He created what I consider to be the most beautiful piece of mathematics ever—the theory of numbers and games—in addition to his seminal work on group theory.
I just noted that all three are somewhat mavericks. For instance, Milner and Kahn never got Ph.D.s, and Conway became famous by scooping the group-theory establishment out of the discovery of a couple of remarkably simple groups. I guess I view research as kind of an adventure.
Q: It seems likely that you will increasingly be asked for advice from aspiring researchers. What is the best bit of professional advice you have received?
Gonthier: A bit of wisdom from my first boss at Bell Labs, Ravi Sethi, keeps popping up in my head. He said: “You know, it [research] is not about problem solving. It’s about problem selection.”
Mathematics