pocklington(1)

pocklington1

Generate a pocklington primality certificate for a prime number

Usage

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

Overview

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.

Releases

Unchanged in 2 releases since Debian 12 (Bookworm).

  1. 12–13

From coqprime-tools 8.20.1-1+b4 in Debian 13 (Trixie). Parsed by carta from the page's man source.