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, EulerFermat
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 treelike 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 cputime, you can even send us your prime
number, we will do the job for you.

