Posted by: Alexandre Borovik | October 13, 2012

Feit-Thompson theorem has been totally checked in Coq

An announcement is here. A quote:

From Laurent Théry
Date: Thursday 20 September 2012, 20:24
Re: [Coqfinitgroup-commits] r4105 – trunk


Just for fun

Feit Thompson statement in Coq:

Theorem Feit_Thompson (gT : finGroupType) (G : {group gT}) : odd #|G| -> solvable G.

How is it proved?

You can see only green lights there:

and the final theory graph at:

How big it is:

Number of lines ~ 170 000
Number of definitions ~15 000
Number of theorems ~ 4 200
Fun ~ enormous!

— Laurent





  1. I find the objections stated in rather convincing.

    And it worries me that Coq developers appear to not to worry much about exploits, although I am unqualified to judge the actual risks.
    Re: proving _anything_ in the Coq proof assistant (in addition to code execution). “coqchk” passes too
    From: Andreas Bogk
    Date: Tue, 03 May 2011 14:55:47 +0200
    Moral: plugins are part of your trusted computing base. You need to trust them
    as much as you need to trust Coq. The good news here is that it requires a
    malicious attacker with write access to the source code to pull off such an attack, whereas finding all genuine bugs would already improve security a lot. And defending against the attack boils down to checking for malicious plugins,
    which falls into line with defending against compiler backdoors, trojaned
    compile hosts etc. “Reflections on trusting trust”, et al.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s


%d bloggers like this: