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.


Categories

Follow

Get every new post delivered to your Inbox.

Join 74 other followers

%d bloggers like this: