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

[Jesse Alama <alama@stanford.edu>]

Thought I'd forward this along to the mizar list, even though it
superficially has to do with Coq.  The web page mentioned in the message
refers to mizar.

Jesse

--- Begin Message ---

• To: coq-club@pauillac.inria.fr
• Subject: Elliptic curve in Coq
• From: Thery Laurent <thery@ns.di.univaq.it>
• Date: Mon, 16 Apr 2007 11:18:47 +0200 (CEST)
• Approved: news@gmane.org
• Archived-at: <http://permalink.gmane.org/gmane.science.mathematics.logic.coq.club/1489>
• Envelope-to: gsmlcc-coq-club@gmane.org
• List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
• Newsgroups: gmane.science.mathematics.logic.coq.club
• Original-received: from discorde.inria.fr ([192.93.2.38]) by lo.gmane.org with esmtp (Exim 4.50) id 1HdNMp-0008Uh-Kb for gsmlcc-coq-club@gmane.org; Mon, 16 Apr 2007 11:19:23 +0200
• Original-received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l3G9JFds010152; Mon, 16 Apr 2007 11:19:15 +0200
• Original-received: from pauillac.inria.fr (localhost.inria.fr [127.0.0.1]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA06611; Mon, 16 Apr 2007 11:19:12 +0200 (MET DST)
• Original-received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA05492 for <coq-club@pauillac.inria.fr>; Mon, 16 Apr 2007 11:18:34 +0200 (MET DST)
• Original-received: from ns.di.univaq.it (ns.di.univaq.it [193.204.130.2]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l3G9IXUM031635 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for <coq-club@pauillac.inria.fr>; Mon, 16 Apr 2007 11:18:34 +0200
• Original-received: from ns.di.univaq.it (localhost.localdomain [127.0.0.1]) by ns.di.univaq.it (8.13.4/8.13.4) with ESMTP id l3G9Ilqh028383 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for <coq-club@pauillac.inria.fr>; Mon, 16 Apr 2007 11:18:47 +0200
• Original-received: from localhost (thery@localhost) by ns.di.univaq.it (8.13.4/8.13.6/Submit) with ESMTP id l3G9IlLi028380 for <coq-club@pauillac.inria.fr>; Mon, 16 Apr 2007 11:18:47 +0200
• Original-sender: coq-club-admin@pauillac.inria.fr
• Original-x-from: coq-club-admin@pauillac.inria.fr Mon Apr 16 11:19:31 2007
• Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:1489

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

--- End Message ---

-- 
Jesse Alama (alama@stanford.edu)
*121: Disagreement of argument types (http://www.mizar.org)