Re: [mizar] [gmane.science.mathematics.logic.coq.club] Elliptic curve in Coq

[Freek Wiedijk <freek@cs.ru.nl>]

Dear all,

>Of course, we will completely cooperate in it.  However,
>we need a systematic map.
>A lot of tools are necessary for it. 

Are we talking about a Mizar-only project here, or more
something like Flyspeck in which different systems are used
for different fragments of the problem?

Not that I have a clear preference either way.  I just like
to know what people are thinking about here.

Freek