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