Pratt’s primality certificates

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Pratt’s primality certificates.

Su autores son Simon Wimmer y Lars Noschinski (Technische Universität München).

El artículo se ha publicado el 22 de julio en el Archive of Formal Proofs.

Su resumen es

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.