The Feit-Thompson theorem checked in Coq!

The Feit-Thompson Theorem  is a key result in the theory of finite groups. Its original proof is 255 pages long and is perhaps the first example of a very long and highly complex proof in group theory.

At 5:46 p.m. on September 20, Georges Gonthier sent an email to his colleagues at the Microsoft Research-Inria Joint Centre in Paris announcing the completion of a six-year effort to prove the Feit-Thompson Theorem in the Coq proof assistant. The mail read, in full: “This is really the End.”

You can read more about this work here and here. 

Congratulations to Georges and his coworkers on this monumental achievement!