.TH POCKLINGTON 1 "July 15th, 2022" .SH NAME pocklington \- generate a Pocklington primality certificate for a prime number .SH SYNOPSIS .B pocklington .RI [-o\ filename] .RI prime .br .B pocklington .RI [-o\ filename] .RI -next\ num .br .B pocklington .RI [-o\ filename] .RI -size\ s .br .B pocklington .RI [-o\ filename] .RI -proth\ k\ n .br .B pocklington .RI [-o\ filename] .RI -lucas\ n .br .B pocklington .RI [-o\ filename] .RI -mersenne\ n .br .B pocklington .RI [-o\ filename] .RI -dec\ filename .br .SH DESCRIPTION This tool takes a prime number and (tries to) generate a Pocklington primality certificate. .SH OPTIONS .B \-v Enable verbose mode .B \-o Prints the proof script in the file named (otherwise the name depends on the way the prime was given) .TP .B A prime number. The default output filename is either prime.v or, if it's too long, Prime.v .TP .B \-next Generate a certificate for the next prime number following . The default output filename is as if the right number had been given. .TP .B \-size Generate a certificate for a prime number with at least decimal digits. The default output filename is as if the right number had been given. .TP .B \-proth Generate a certificate for the Proth number k*2^n+1. The default output filename is as if the right number had been given. .TP .B \-lucas Generate a certificate for the Mersenne number 2^n-1 using Lucas' test (more efficient). The default output filename is lucas.v. .TP .B \-mersenne Generate a certificate for the Mersenne number 2^n-1 using Pocklington's test. The default output filename is mersenne.v. .TP .B \-dec Generate a certificate for the number given in the file ; the file should also contain a partial factorization of the predecessor. The output filename is .v.