Subject: [Math-visitors] remarkable achievement in proof verification

Date: Wed, 17 Oct 2012 13:22:57 -0400

From: Jean Gallier <jean@cis.upenn.edu>

To: faculty@math.upenn.edu, grad@math.upenn.edu, visitors@math.upenn.edu

Dear all,

I learned from the "Types Forum" that a group of researchers at MSR/INRIA

led by Georges Gonthier completed a formal verification (in Coq) of the

"Odd order theorem," due to Feit and Thompson

(every finite group of odd order is solvable).

The task of proof verification in Coq took 6 years. The Coq development contains

~ 170 000 lines of code

~ 4200 definitions

~ 15 000 theorems.

They did find small gaps, but all could be patched.

For more details, see

http://www.msr-inria.inria.fr/Projects/math-components/feit-thompson

In particular, at the end of the page, look at the "final theory graph."

The question remains: how do we know (and prove) that Coq is correct?

We have to verify the verifier!

Best,

-- Jean ]]>