At 5:46 p.m. on Sept. 20, Georges Gonthier, principal researcher at Microsoft Research Cambridge, sent a brief email to his colleagues at the Microsoft Research-Inria Joint Centre in Paris. It read, in full:
“This is really the End.”
Those five innocuous words heralded the culmination of a project that had consumed more than six years and resulted in the formal proof of the Feit-Thompson Theorem, the first major step of the classification of finite simple groups.
The theorem, first proved by Walter Feit and John Griggs Thompson in 1963 and also known as the Odd-Order Theorem, states that in mathematical group theory, every finite group of odd order is solvable.
That might seem a deceptively simple definition to non-mathematicians, but Gonthier and his collaborators on the Mathematical Components project at the Microsoft Research-INRIA Joint Centre are anything but. Their achievement in completing a computer-assisted proof by the Coq proof assistant, developed atInria, the French National Research Institute for Computer Science and Applied Mathematics, was acclaimed widely as news spread.
Michel Cosnard, Inria chairman of the board and CEO, was quick to commend the development.
“My deepest congratulations for this beautiful and amazing piece of work,” he wrote. “Of course, Georges Gonthier and his team deserve our full consideration. But I would also underline the quality of the Microsoft Research-Inria partnership, which gave to them the absolutely necessary conditions for climbing this Everest.”