### Abstract

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.

### License

BSD License

### Topics

- Computer science/Algorithms/Randomized
- Mathematics/Number theory

### Session Probabilistic_Prime_Tests

- Legendre_Symbol
- Algebraic_Auxiliaries
- Jacobi_Symbol
- Residues_Nat
- QuadRes
- Euler_Witness
- Carmichael_Numbers
- Fermat_Witness
- Generalized_Primality_Test
- Fermat_Test
- Miller_Rabin_Test
- Solovay_Strassen_Test

### Used by

- Mersenne primes and the Lucas–Lehmer test

## Cite

×

Probabilistic_Prime_Tests-AFP

    @article{Probabilistic_Prime_Tests-AFP,
      author  = {Daniel Stüwe and Manuel Eberl},
      title   = {Probabilistic Primality Testing},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Probabilistic_Prime_Tests.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Feb 15, 2019 : Isabelle2018