The Coq mailing list

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

Hi,

for people who are interested in the formalisation of Fermat last 
theorem

http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html

Formalising elliptic curves, the easy first bit :-), has been done
inside  Coq

It has been used to prove the primality of prime numbers using 
Aitkin-Goldwasser-Kilian-Morain certificate:
http://mathworld.wolfram.com/Atkin-Goldwasser-Kilian-MorainCertificate.html

Now we can prove the primality within Coq of any prime with less than 300
decimal digits.

All the code for elliptic curve is available here

http://coqprime.gforge.inria.fr/

under the directory elliptic and compiles with Coq 8.1

--
Laurent