Abstract: 
This article provides formal proofs of basic properties of
Mersenne numbers, i. e. numbers of the form
2^{n}  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. 
BibTeX: 
@article{Mersenne_PrimesAFP,
author = {Manuel Eberl},
title = {Mersenne primes and the Lucas–Lehmer test},
journal = {Archive of Formal Proofs},
month = jan,
year = 2020,
note = {\url{http://isaafp.org/entries/Mersenne_Primes.html},
Formal proof development},
ISSN = {2150914x},
}
