Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Probabilistic Primality Testing


view this post on Zulip Email Gateway (Aug 22 2022 at 19:10):

From: Tobias Nipkow <nipkow@in.tum.de>
Probabilistic Primality Testing
Daniel Stüwe and Manuel Eberl

The most efficient known primality tests are probabilistic in the sense that
they use randomness and may, with some probability, mistakenly classify a
composite number as prime – but never a prime number as composite. Examples of
this are the Miller–Rabin test, the Solovay–Strassen test, and (in most cases)
Fermat's test.

This entry defines these three tests and proves their correctness. It also
develops some of the number-theoretic foundations, such as Carmichael numbers
and the Jacobi symbol with an efficient executable algorithm to compute it.

https://www.isa-afp.org/entries/Probabilistic_Prime_Tests.html

Enjoy!
smime.p7s


Last updated: Apr 24 2024 at 01:07 UTC