Pocklington

Coq formalization of Pocklington's criterion for checking primality of large natural numbers. Includes a formal proof of Fermat's little theorem.

Meta

• Author(s):
  • Olga Caprotti (initial)
  • Martijn Oostdijk (initial)
• Coq-community maintainer(s):
  • Pierre Castéran (@Casteran)
• License: GNU Lesser General Public License v2.1 or later
• Compatible Coq versions: 8.7 or later
• Additional dependencies: none
• Coq namespace: Pocklington
• Related publication(s):
  • Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles doi:10.1006/jsco.2001.0457

Building and installation instructions

The easiest way to install the latest released version of Pocklington is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-pocklington

To instead build and install manually, do:

git clone https://github.com/coq-community/pocklington.git
cd pocklington
make   # or make -j <number-of-cores-on-your-machine> 
make install