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

# firstprimes(1)

primality certification for the first primes

## NAME

firstprimes - primality certification for the first primes

## SYNOPSIS

**firstprimes** \[-o filename\] -base maxindex\
 **firstprimes** \[-o filename\] minindex maxindex\

## DESCRIPTION

This tool outputs in the file filename (default: FirstPrimes.v) the proof of primality for the primes between the minimum and the maximum indexes.

It contains a rather large list (thousands) of the first primes, and is able to output a proof of primality for each of them ; the indexes are relative to this list.

## OPTIONS

**-o \<filename\>** Prints the proof script in the file named \<filename\> (otherwise: FirstPrimes.v)

- **-base \<maxindex\>**

  Gives proofs for the primes from 0 (included) to \<maxindex\> (excluded)

- **\<minindex\> \<maxindex\>**

  Gives proofs for the primes from \<minindex\> (included) to \<maxindexoo\> (excluded)