### Abstract

This article provides formal proofs of basic properties of Mersenne numbers, i. e. numbers of the form 2n - 1, and especially of Mersenne primes.

In particular, an efficient, verified, and executable version of the Lucas–Lehmer test is developed. This test decides primality for Mersenne numbers in time polynomial in n.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Mersenne_Primes

- Lucas_Lehmer_Auxiliary
- Lucas_Lehmer
- Lucas_Lehmer_Code

### Depends on

- Native Word
- Pell’s Equation
- Probabilistic Primality Testing

## Cite

×

Mersenne_Primes-AFP

    @article{Mersenne_Primes-AFP,
      author  = {Manuel Eberl},
      title   = {Mersenne primes and the Lucas–Lehmer test},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Mersenne_Primes.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
- Jan 20, 2020 : Isabelle2019