How to formally and efficiently prove primality of large numbers

Olga Caprotti & Martijn Oostdijk

Eindhoven University of Technology


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.