I probably don't have the appropriate background to even ask this question. I know next to nothing about formal or computer-aided proof, and very little even about group theory. And this question is more "tech support" than math.

But: after reading that Georges Gonthier and collaborators had formalized a proof of the Feit-Thompson theorem in Coq, I thought it would be fun to try to verify it on my own computer.

So I installed Coq (8.4pl2), OCaml, etc, on my Ubuntu box, and then went here and downloaded `feit_thompson.tar.gz`

(v2.0). I unpacked it and ran `make`

. It ran various invocations of `coqc`

for about two hours, and then finished with no error reported. A bunch of `.vo`

files were produced, including one for `theories/stripped_odd_order_theorem.v`

, which even the casual observer can see contains what appears to be a statement of the Feit-Thompson theorem.

Is that it? Does that mean that Coq agrees with the correctness of the proof? Or are there more steps?

I was particularly curious because I saw that `Makefile.coq`

has a `validate`

target (which isn't run by just doing `make`

). So I ran `make -f Makefile.coq validate`

. This started a `coqchk`

command which ran for about five minutes and then *failed* with:

```
User error: Signature components for label fun_of_fin do not match
make: *** [validate] Error 1
```

Was I not supposed to do that? Or did I just find a flaw in their proof? :-)

Again, I freely admit that I do not really know what I'm doing. In particular, it's not clear to me whether compilation of a Coq file actually verifies the theorems and proofs within it, or merely prepares it for later validation. If an expert answers "Go away until you understand Coq" I'll meekly accept it. But it does seem like it might be helpful for even a newbie to be able to understand how to properly run Coq on a proof created by someone else, and I couldn't find documentation that clearly explained it.

15more comments