---
name: "pocklington"
section: "1"
platform: "linux"
package: "coqprime-tools"
version: "8.20.1-1+b4"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/pocklington"
---

# pocklington(1)

generate a Pocklington primality certificate for a prime number

## NAME

pocklington - generate a Pocklington primality certificate for a prime number

## SYNOPSIS

**pocklington** \[-o filename\] prime\
 **pocklington** \[-o filename\] -next num\
 **pocklington** \[-o filename\] -size s\
 **pocklington** \[-o filename\] -proth k n\
 **pocklington** \[-o filename\] -lucas n\
 **pocklington** \[-o filename\] -mersenne n\
 **pocklington** \[-o filename\] -dec filename\

## DESCRIPTION

This tool takes a prime number and (tries to) generate a Pocklington primality certificate.

## OPTIONS

**-v** Enable verbose mode **-o \<filename\>** Prints the proof script in the file named \<filename\> (otherwise the name depends on the way the prime was given)

- **\<prime\>**

  A prime number. The default output filename is either prime\<prime\>.v or, if it's too long, Prime.v

- **-next \<num\>**

  Generate a certificate for the next prime number following \<num\>. The default output filename is as if the right number had been given.

- **-size \<s\>**

  Generate a certificate for a prime number with at least \<s\> decimal digits. The default output filename is as if the right number had been given.

- **-proth \<k\> \<n\>**

  Generate a certificate for the Proth number k\*2^n+1. The default output filename is as if the right number had been given.

- **-lucas \<n\>**

  Generate a certificate for the Mersenne number 2^n-1 using Lucas' test (more efficient). The default output filename is lucas\<n\>.v.

- **-mersenne \<n\>**

  Generate a certificate for the Mersenne number 2^n-1 using Pocklington's test. The default output filename is mersenne\<n\>.v.

- **-dec \<filename\>**

  Generate a certificate for the number given in the file \<filename\> ; the file should also contain a partial factorization of the predecessor. The output filename is \<filename\>.v.