This lecture of the Digiteo seminar is organised in common with the Math department of the Université Paris-Sud

This lecture is about the proof in Coq of the Feit-Thompson theorem.

This theorem, also named the Odd Order Theorem, is the first main result in the classification of finite groups.This work was achieved by the team led by Georges Gonthier. It is the result of a 6-year long research effort (almost fulltime work) started in May 2006. After the Four Color theorem, this is the second impressive mathematical theorem totally proved in the Coq proof assistant.