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

Hi,

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:

http://ssr2.msr-inria.inria.fr/~jenkins/current/progress.html

and the final theory graph at:

http://ssr2.msr-inria.inria.fr/~jenkins/current/index.html

How big it is:

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

– Laurent

 

 

About these ads

Responses

  1. I find the objections stated in http://mathoverflow.net/questions/18421/how-do-they-verify-a-verifier-of-formalized-proofs 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.

    http://seclists.org/fulldisclosure/2011/May/73
    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:

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

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

Connecting to %s

Categories

Follow

Get every new post delivered to your Inbox.

Join 77 other followers

%d bloggers like this: