Mersenne Primes and the Lucas–Lehmer Test

Manuel Eberl

17 January 2020


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.

BSD License

Depends On