81

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.

Lee Mosher
  • 15,334
Nate Eldredge
  • 29,204
  • 25
    I like this question, and would defend it against potential voters-to-close (saying "ask in a Coq forum") by saying that this is the sort of activity (downloading and stepping through a proof certificate) that the proof assistant community, and others in the pure mathematics community (e.g. Voevodsky) are hoping would be the standard method of checking a proof in mathematics in the future. – David Roberts May 02 '14 at 03:19
  • from memory, you need something like Proof General (in emacs) or CoqIDE to 'run' the .v file - it will show you the internal proof state as you step through the file and will let you know that the proof of each theorem is accepted. – David Roberts May 02 '14 at 03:22
  • 9
    I'm not going to vote to close, but I don't think MO is the right place for this sort of question in the long run. Questions about how to express a proof in a way understandable to Coq or about the limitations of Coq seem germane, but we should probably find another home for tech support questions like this for the same reason that we don't typically allow Latex or Mathematica questions. – Paul Siegel May 02 '14 at 03:41
  • 2
    I think the reason why we don't allow LaTeX questions is the existence of http://tex.stackexchange.com/ . I don't know if something like this can be said of Coq; I assume the closest thing would be http://cstheory.stackexchange.com/ , but there is virtue in bringing up these issues in a mathematical forum as well. – darij grinberg May 02 '14 at 04:35
  • There surely is a Coq user mailing list. And whoever wrote feit_Thompson.tar.gz is a great candidate to be sent an email asking what his package is supposed to do :-) – Mariano Suárez-Álvarez May 02 '14 at 05:14
  • 11
    It has long been agreed that the non-existence of a Q&A site for subject X is not reason for X to be on topic here, btw. – Mariano Suárez-Álvarez May 02 '14 at 05:16
  • 5
    @MarianoSuárez-Alvarez: The coq mailing list is a good idea, though it seems more aimed at formal proof experts than newbie working mathematicians. I thought an answer to this question might be useful information for the MO community; there have been several previous questions here about Coq and they were generally well received. As far as asking the authors, I certainly could, but in principle the goal is for me to be able to verify the proof independently; I don't want to have to take the author's word for how to do it. – Nate Eldredge May 02 '14 at 05:19
  • Compilation of coq files is not enough. If coqchk fails, there is something wrong, possibly with coq component. Coq fixed some critical bugs for assumption free proofs of False. – joro May 02 '14 at 07:05
  • As far as the question whether there SE sites where (at least some) questions on Coq would be appropriate, some such questions have been asked and answered on Math.SE. Simply search for coq or the tags theorem-provers and computer-assited-proofs to see some such questions. This Google search shows that cstheory has a coq tag and some questions. – Martin Sleziak May 02 '14 at 07:26
  • 2
    In any case, the discussion where questions related to Coq should be asked and whether they are on-topic on this site seems to be more suitable for meta (or chat) than comments to this particular question. – Martin Sleziak May 02 '14 at 07:27
  • I was aware that it is not optimal to let MO be the target for Coq questions (and I thought about the analogy with computer algebra packages), but since this is a new and developing part of mathematics, it is worth having at least one question, to which answers could include what it means for a person to 'run' a Coq proof, mathematically. Nitty-gritty details of makefiles is less useful and I agree better suited to a Coq-specific forum. – David Roberts May 02 '14 at 10:50
  • Here is the second question: http://mathoverflow.net/questions/164947/where-can-i-find-gonthiers-coq-code-proving-the-four-color-theorem. – Dietrich Burde May 02 '14 at 11:24
  • The proof contains axioms, so you might want to check them too. – joro May 02 '14 at 15:10
  • 2
    @DavidRoberts could you finally create a meta thread if you want to continue to discuss this. And, as a reminder, comments against closure before even a vote was cast (except there should been one that got canceled) are considered bad form. –  May 02 '14 at 15:55
  • think this is on topic but admittedly very unusual. (there are some questions on [cstheory.se] on auto thm proving systems & even one highvoted one on Gonthier Feit-Thompson although they might not go for this one.) it would appear from your description that the project (basically verging on a software package) has poor documentation. a not-uncommon scenario for software projects & esp an issue with many open source systems. ie does it even have a README? – vzn May 02 '14 at 16:57
  • 2
    Meta thread: http://meta.mathoverflow.net/questions/1672 – David Roberts May 03 '14 at 05:34
  • Since I am curious, I did the same thing and ran into a "Error: Unbound module Genarg". It is embarassing that a proof runs fine or not depending on an implementation :-) (Ubuntu 14.04 with the coq and ocaml packages provided with it). Will one be able to run the proof again in 10 years ? – Philippe Gaucher May 07 '14 at 09:35
  • 2
    @PhilippeGaucher: I had this same problem. The message is cryptic, but it actually just indicates a missing file. You have to install the libcoq-ocaml-dev package. – Nate Eldredge May 07 '14 at 16:18
  • I also just learned that Coq is also discussed on Stack Overflow. – Nate Eldredge Nov 13 '15 at 15:45
  • @NateEldredge: Having this experiment easily reproducible could make a very good answer to my question at http://math.stackexchange.com/questions/1607517 ... – Olexandr Konovalov Jun 17 '16 at 22:30

3 Answers3

54

The error you get is a real one, but is not in the proof of the odd order theorem. It is in Coq. Let me be more clear: a bug in the kernel of Coq was making the .vo files (the files coqchk checks) incomplete. Some universe constraints coming from module sub typing were forgotten. coqchk correctly spots it, and actually revealed the bug I fixed a while ago. A patchlevel release of Coq including the fix is already on its way.

The bugreport: https://coq.inria.fr/bugs/show_bug.cgi?id=3243

The commit that fixed the bug: https://github.com/coq/coq/commit/a07deb4eac1d5f886159784ef5d8d006892be547

Enrico Tassi
  • 556
  • 2
    Many thanks, I don't know how I would have found that myself. So just to be clear, the compilation alone did not verify the proof? – Nate Eldredge May 02 '14 at 16:55
  • 16
    @NateEldredge I believe the way to understand this is: make checked the proof, and compiled it to an optimized version; however, because the compilation phase was buggy, the optimized version was not a correct proof. When you ran make validate, coqchk tried to check the optimized proof, but barfed because the optimized proof produced by Coq earlier was not an accurate reflection of the original proof. – Daniel Wagner May 02 '14 at 18:45
  • 1
    @DanielWagner: Thanks, that makes it very clear. – Nate Eldredge May 02 '14 at 18:56
26

Following Enrico Tassi's answer, I compiled the current snapshot of Coq 8.4pl4 from https://github.com/coq/coq. With it, I was able to successfully compile and validate the proof.

 Modules were successfully checked

What an impressive piece of work!

Nate Eldredge
  • 29,204
  • What does it do/look like when you validate the proof? – David Roberts May 03 '14 at 01:56
  • 8
    @DavidRoberts: At the end of make validate it prints the Modules were successfully checked message, and a list of the axioms used. (By default it runs with -silent; I turned that off so I also got a running list of the theorems/lemmas as they were verified. It took about one hour to run.) – Nate Eldredge May 03 '14 at 02:21
25

To convince yourself that the proof is indeed valid, you need to do at least two things:

  • read and understand the definitions as well as the theorem statement thus knowing for a fact that the proof is indeed a proof of the right theorem;

  • check the development using a proofchecker you trust.

Now, that second part can be a bit tricky: coqc is quite a big piece of code allowing the use of plugins, the definition of custom tactics, etc. That's why a standalone checker coqchk exists: it can only deal with compiled files (i.e. raw proof terms) and therefore is much simpler thus making it easier to review its code.

It is bothering that coqchk fails on this development. It would be worth mentioning either on coq's bug tracker or on the ML.

gallais
  • 455