Probabilistic_Prime_Tests swMATH ID: 38026 Software Authors: Daniel Stüwe; Manuel Eberl Description: Probabilistic_Prime_Tests: Probabilistic Primality Testing. 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. Homepage: https://www.isa-afp.org/entries/Probabilistic_Prime_Tests.html Dependencies: Isabelle Related Software: Isabelle/HOL; Monad normalisation; Density Compiler; Random BSTs; Root Balanced Tree; Treaps; QuickSort Cost; Archive Formal Proofs; Amortized Complexity; CryptHOL; Ergodic theory; Quicksort; HOL; Isabelle Cited in: 1 Document Cited by 3 Authors 1 Eberl, Manuel 1 Haslbeck, Max W. 1 Nipkow, Tobias Cited in 1 Serial 1 Journal of Automated Reasoning Cited in 1 Field 1 Computer science (68-XX) Citations by Year