Ssreflect Users Discussion List

[Kevin Buzzard <>]

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.

I am a pure mathematician with some unix experience (so not scared of
typing "make" or learning about opam) and some programming experience,
but no functional programming experience. I would like to learn more
about what computers can currently do when it comes to
theorem-checking and theorem-proving. 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; of course one possibility is that I push on and then
write the guide myself.

At my university we teach 3rd year courses in group theory, Galois
theory and representation theory, and although I have been aware for
years that Gonthier et al have verified Feit-Thompson, I have only
just learnt that (unsurprisingly) verifying several of the main
results in these undergraduate level courses was a substantial part of
the work. 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), with tactics which have already been
formalised by other people, and I figured that the best way to find
out was to try and solve some myself. 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.

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.

**

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.