### Abstract

In 1975, Pratt introduced a proof system for certifying primes. He showed that a number p is prime iff a primality certificate for p exists. By showing a logarithmic upper bound on the length of the certificates in size of the prime number, he concluded that the decision problem for prime numbers is in NP. This work formalizes soundness and completeness of Pratt's proof system as well as an upper bound for the size of the certificate.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Pratt_Certificate

- Pratt_Certificate
- Pratt_Certificate_Code

### Depends on

- Lehmer’s Theorem

### Used by

- Amicable Numbers
- Bertrand’s postulate

### Auto-related entries

- A Sequent Calculus Prover for First-Order Logic with Functions
- Szemerédi’s Regularity Lemma
- Expected Shape of Random Binary Search Trees

## Cite

×

Pratt_Certificate-AFP

    @article{Pratt_Certificate-AFP,
      author  = {Simon Wimmer and Lars Noschinski},
      title   = {Pratt's Primality Certificates},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Pratt_Certificate.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Jul 29, 2013 : Isabelle2013