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.001s 
9 
61 
19 
1883 
Pervushin 
0.001s 
10 
89 
27 
1911 
Powers 
0.001s 
11 
107 
33 
1914 
Powers 
0.002s 
12 
127 
39 
1876 
Lucas 
0.003s 
13 
521 
157 
1952 
Robinson 
0.06s 
14 
607 
183 
1952 
Robinson 
0.08s 
15 
1279 
386 
1952 
Robinson 
0.63s 
16 
2203 
664 
1952 
Robinson 
2.22s 
17 
2281 
687 
1952 
Robinson 
2.38s 
18 
3217 
969 
1957 
Riesel 
5.08s 
19 
4253 
1281 
1961 
Hurwitz 
11.92s 
20 
4423 
1332 
1961 
Hurwitz 
13.03s 
21 
9689 
2917 
1963 
Gillies 
100.36s 
22 
9941 
2993 
1963 
Gillies 
106.62s 
23 
11213 
3376 
1963 
Gillies 
140.28s 
24 
19937 
6002 
1971 
Tuckerman 
643.78s 
25 
21701 
6533 
1978 
Noll
& Nickel 
797.97s 
26 
23209 
6987 
1979 
Noll
& Nickel 
927.54s 
27 
44497 
13395 
1979 
Nelson
& Slowinski 
5204.90s 
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.

