The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

> Has anyone done any of the theory of elliptic curves in Coq?

I've just been starting a formalisation to apply it to number theory but I 
haven't gone very far (I'm stuck in the proof that the group operation is 
associative). Otherwise Marie Virat (<virat AT math.unice.fr>) did some stuff 
with elliptic curve in Coq. Also Joe Hurd (<joe.hurd AT comlab.ox.ac.uk>) 
did something but in the HOL prover.

--
Laurent Théry