Welcome to the coqfinitgroup home page,

The formal proof of the Feit-Thompson theorem has been completed on September 20, 2012.

You can download the archive of the proof

You can browse

• the documentation of version v1.0
• some figures about version v1.0
• the library corresponding to ssreflect-1.4
• the library corresponding to ssreflect-1.3
• the library corresponding to ssreflect-1.2