# How to formally and efficiently prove primality of large numbers

## Olga Caprotti & Martijn Oostdijk

## Eindhoven University of Technology

### ABSTRACT

In this talk I will present some recent work in formalizing
Pocklington's Criterion for testing primality of numbers.
We formalized this criterion in the proofassistant Coq.
Computer algebra systems such as GAP and Maple can be used
to provide the necessary witnesses for applying the criterion.
The medium used for communication between these systems is the
OpenMath language.

The formalization in Coq is interesting because we were forced to
prove a large amount of trivial and less trivial results which are
usually not explicitly mentioned in the informal proof.
It is clear after this experiment that still a lot of work needs to be done
before one is able to reach the conciseness of informal mathematics.

If time permits, I will give a short system demo.