Welcome to CoqPrime project!

Certifying Prime Number with the Coq prover

CoqPrime is a library built on top of the Coq proof system to certify primality using Pocklington certificate and Elliptic Curve Certificate. It is a nice illustration of what we can do with safe computation inside a prover. The library consists of 4 main parts:

A library of facts from number theory: the goal was to prove the theorems relative to Pocklington certificate. The library includes some very nice theorems like Lagrange theorem, Euler-Fermat theorem.
A library for elliptic curves
An efficient library to perform modular arithmetic: using the standard representation of integers in Coq was not sufficient to tackle large prime numbers so we have developped our own modular arithmetic based on tree-like structures. The library includes comparison, successor, predecessor, complement, addition, subtraction, multiplication, square, division, square root, gcd, power and modulo.
A C program that generates Pocklington certificates. This program is based on ECM and some scripts that turn a certificate generated by primo into a Coq file

Here are the benchmark for some Mersenne numbers

#	n	digits	years	discoverer	checking time
8	31	10	1772	Euler	0.01s
9	61	19	1883	Pervushin	0.01s
10	89	27	1911	Powers	0.02s
11	107	33	1914	Powers	0.02s
12	127	39	1876	Lucas	0.04s
13	521	157	1952	Robinson	1.85s
14	607	183	1952	Robinson	2.78s
15	1279	386	1952	Robinson	20.21s
16	2203	664	1952	Robinson	89.1s
17	2281	687	1952	Robinson	97.59s
18	3217	969	1957	Riesel	237.65s
19	4253	1281	1961	Hurwitz	494.09s
20	4423	1332	1961	Hurwitz	563.27s
21	9689	2917	1963	Gillies	5304.08s
22	9941	2993	1963	Gillies	5650.63s
23	11213	3376	1963	Gillies	7607.00s
24	19937	6002	1971	Tuckerman	34653.12s
25	21701	6533	1978	Noll & Nickel	43746.21s
26	23209	6987	1979	Noll & Nickel	51210.56s
27	44497	13395	1979	Nelson & Slowinski	282784.09s

If you have a number you really want to be sure that it is prime

what should you do?
If your number has less than 100 decimal digits:

Download and compile the library

Generate the cerficate for your prime number. For example for 1234567891, the command pocklington 1234567891 generates the file

Require Import PocklingtonRefl.
Set Virtual Machine.
Open Local Scope positive_scope.
Lemma prime1234567891 : prime 1234567891.
Proof.
apply (Pocklington_refl
(Pock_certif 1234567891 2 ((3607, 1)::(2,1)::nil) 12426)
((Proof_certif 3607 prime3607) ::
(Proof_certif 2 prime2) ::
nil)).
exact_no_check (refl_equal true).
Qed.

Compile the file with coqc

If your number has more than 100 decimal digits

Download and compile the library
Use primo to generate a cerficiate file.out (the certificate for 1234567890123456789012353). Use the command o2v to generate the file file.v (the file for 1234567890123456789012353). and use the script v2v to add a wrapper aroung the file file.v (the final file for 1234567890123456789012353).
Compile the file with coqc

Proving the primality of a number of about 300 decimal digits takes about an hour (see Research Report).

If you are too lazy to install the Coq system, or have no spare cpu-time, you can even send us your prime number, we will do the job for you.

Project Summary

Tracker

- Bugs(0 open / 0 total)

- Support Requests(0 open / 0 total)

- Patches(2 open / 2 total)

- Feature Requests(0 open / 0 total)