Ssreflect Users Discussion List

[Assia Mahboubi <>]

Dear Kevin,

  many thanks for your interest in this work, and for the time you took to
provide feedback. It is very useful.

Le 14/06/2017 à 17:05, Kevin Buzzard a écrit :
> Aah I see my mistake. I misunderstood your original answer as saying
> "ssreflect is in mathcomp" . I knew that ssreflect was part of
> mathcomp, however I had not realised that the Feit-Thompson work was
> also part of mathcomp. This is great news; many thanks and apologies
> for misunderstanding you earlier.

Well, this is more an unfortunate confusing name clash, to blame on us 
probably,
than a mistake of yours... Let me try to clarify :

- Mathematical components is the name of a formalisation project and of a set 
of
libraries. It was originally chosen by Georges Gonthier for his team at the
Microsoft Inria Joint Centre. The idea was to highlight the similarities 
between
software engineering techniques used to make large pieces of software work and
last, and an appropriate methodology for building libraries of formalised
mathematics.

- math-comp is the name of a github so-called "organisation", which showcases
some formalisation projects built with this methodology in mind:

https://github.com/math-comp

- the main project hosted by he math-comp organization is itself called 
math-comp :

https://github.com/math-comp/math-comp

and this git repository contains the sources of the so called Mathematical
Components libraries. The libraries include, among other things, a complete
formal proof of the odd order theorem, but also a few other things.

- the Mathematical Components libraries are thus a rather large body of Coq
code, which takes some time to be compiled. It is thus broken down into 
several
groups of files, stored in distinct sub-directories, so that people can used
only the relevant subset of libraries for their needs.

- today, the preferred way to install external libraries for Coq is via the 
opam
package manager. opam is not specific to coq, it is meant to handle the
installation of libraries of the ocaml ecosystem. There is thus a naming 
policy
for the special case of opam packages that are in fact coq packages : they are
prefixed with coq-, as you can see in this list :

https://github.com/coq/opam-coq-archive/tree/master/released/packages

of packages. In this list, you also find packages featuring a coq-mathcomp
prefix. These are the packages corresponding to the group of files mentioned 
in
the previous items.

- For a reason I do not understand (I was myself not aware of the issue until
very recently), there is currently no opam package for the complete sources of
the formal proof of the Odd Order theorem. Of course, the files covering the
books by Bender and Glauberman and by Peterfalvi are of a more confidential
interest than the libraries about linear algebra.

> 
> ... I have had to struggle through
> set-ups that are not quite compatible with each other etc and it took
> a while to realise that opam was a better bet than e.g. installing
> from ubuntu sources or compiling from source -- but I feel like every
> day I am making some progress. I still have not found the guide I am
> looking for; 

This is very unfortunate, I am sorry to read this.

> of course one possibility is that I push on and then
> write the guide myself.

This would be awesome of course, but sending us a few lines about what worked
and what didn't is already super useful.
> 
> ... I taught Galois theory until last year; I am now wondering
> how many of my problem sheet questions can be solved by computer (once
> translated into Coq of course),

Is there any way to have access to this teaching material? I could may be try 
to
answer this question, and to give pointers to the Coq code when the answer is
"yes it can". Actually, I would be interested in the answer to this question 
too...

> ... I also wonder how many of the
> 3rd year pure mathematics undergraduate exams at my university are
> currently ready to be tackled by a machine.

This question is probably harder to answer. I do not expect that today all of
this corpus is covered by the libraries of a single proof assistant. But may 
be
is there a covering: for instance the algebra part would be doable with Coq, 
and
the analysis with the HOL-Light or the Isabelle/HOL system (both have been 
used
for verifying Hales'proof of the Kepler conjecture).

> Let me comment that at https://coq.inria.fr/ there is a link called
> Feit-Thompson which points to www.msr-inria.fr, which currently does
> not respond.

Thanks for reporting this!

I will answer the second part of your message in a separate message.

Kind regards,

assia


> Now Emilio has pointed me to the ssreflect mailing list let me explain
> what I believe will be a stumbling-block for me later. My impression
> from reading the Feit-Thompson Coq paper by Gonthier et al is that the
> Coq proof of F-T is all done in "constructible mathematics", so we are
> probably not using the Axiom of Choice. Now if on the other hand one
> were to start considering formalising the proof of Fermat's Last
> Theorem, say, then one would need a whole bunch of delicate real
> analysis (for the trace formula part of the argument where one proves
> that the 3-torsion of an elliptic curve is modular if irreducible) and
> in this part of the argument I am sure that AC will be used a lot. It
> would seem natural to me more generally to start proving results from
> many pure mathematics courses at undergraduate level, assuming one is
> working in a first order theory and working under the axioms of ZFC
> (this is, it seems to me, what is implicitly going on in many
> undergraduate level pure courses). However my impression is that this
> is not what is going on in the Feit-Thompson work. I know that ZFC has
> been implemented in Coq. What I am currently unclear about is
> precisely which axioms were used to prove Feit-Thompson in Coq; my
> current lack of understanding is such that I am currently still
> confused about what role the law of the excluded middle plays. I am
> hoping to understand more over the next few days. I would be very
> interested in any pointers that people may have where I could learn
> more about what one literally means precisely by "the odd order
> theorem has been verified". I suspect that the statement is _not_ "the
> proof was verified in ZFC", however this might well be a consequence
> of what was actually done; I suspect it was verified in a weaker axiom
> system.
> 
> Kevin
> 
> On 14 June 2017 at 15:05, Emilio Jesús Gallego Arias 
> <>
>  wrote:
>> Hi Kevin,
>>
>> [addressing this to the ssreflect list where the true experts on the
>> proof can see it]
>>
>> Kevin Buzzard 
>> <>
>>  writes:
>>
>>> I have the current ssreflect installed and it works fine for me in Coq
>>> 8.6 too. On reflection I think that my question is perhaps for the
>>> maintainers of the Feit-Thompson proof. It had not occurred to me that
>>> one might need to maintain a proof!
>>
>> I am not sure if you are referring to the proof in the old directory,
>> but note that the proof is maintained (and works for me) in the github
>> repository I pointed to:
>>
>> https://github.com/math-comp/math-comp/blob/master/mathcomp/odd_order/stripped_odd_order_theorem.v
>>
>> That is to say, I think that if you use Coq 8.6 you should not rely on
>> the original published file.
>>
>> E.