**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### 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*.