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:
  1. 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.
  2. A library for elliptic curves
  3. 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.
  4. 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:
  1. Download and compile the library
  2. 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.
  3. Compile the file with coqc

If your number has more than 100 decimal digits
  1. Download and compile the library
  2. 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).
  3. 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.
This page is not maintained anymore. Please go to https://github.com/thery/coqprime for a recent version of this library.