[isabelle] New AFP entries: Lehmer's Theorem and Pratt's Certificates

Pratt's Primality Certificates
Simon Wimmer and Lars Noschinski

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.


Lehmer's Theorem
Simon Wimmer and Lars Noschinski

In 1927, Lehmer presented criterions for primality, based on the converse of
Fermat's litte theorem. This work formalizes the second criterion from Lehmer's
paper, a necessary and sufficient condition for primality.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.