Pratt's Primality Certificates

Title:	Pratt's Primality Certificates
Authors:	Simon Wimmer and Lars Noschinski
Submission date:	2013-07-22
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.
BibTeX:	@article{Pratt_Certificate-AFP, author = {Simon Wimmer and Lars Noschinski}, title = {Pratt's Primality Certificates}, journal = {Archive of Formal Proofs}, month = jul, year = 2013, note = {\url{http://isa-afp.org/entries/Pratt_Certificate.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Lehmer
Used by:	Amicable_Numbers, Bertrands_Postulate
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.