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!