A six year research project leads to a major result for mathematics and computer science, highlighting the benefits of academia-industry partnership.
Last September, the Microsoft Research-INRIA Joint Centre in Paris announced that Georges Gonthier and his team have completed a 6-year project that is opening a new page in the history of mathematics and computing. This achievement is a landmark in the very recent history of “mathematical engineering”, a new field which lets mathematicians check their proofs with the help of computers.
Thanks to this work, and thanks to computer science, “mathematical engineering” is becoming a reality! Georges Gonthier and his team certainly deserve all the credit of overcoming the scientific hurdles. But I would also like to underline the quality of the partnership between Microsoft Research and INRIA, the French research centre in Computer Science, which made this possible.
What is the work about? The formalisation of the Feit-Thompson theorem. Unlike the four colour theorem which Georges tackled in 2005 and which attracted the attention of The Economist, the Feit-Thompson theorem is not easily understandable by non-mathematicians. However what’s remarkable about this theorem is the length of the proof which spreads 255 pages, and the fact that the proof involves many deep areas of algebra (character theory, Sylow’s groups theory, etc.). Not surprisingly, for decades the proof has been challenged about its completeness and accuracy. The verification using a computer is an achievement in itself given the complexity. But it also brings an end to the long debate. Furthermore, and that’s the game changer, the team used a modular approach in their work and built a set of components, each formalizing a specific subset of algebra, that the mathematics community will be able to reuse for other proofs. In that sense, mathematicians will be able to do math in a new way.
Alan Turing, one of the fathers of computer science had understood how computing could benefit mathematics and vice versa. Georges is pioneering new interactions between the two sciences: Computer Science provides new ways of formalizing and verifying mathematical proofs; conversely, the elaboration of these methods pushes the frontiers of mathematical logic.