Explicit Mersenne primes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We run some Lucas-Lehmer tests to prove some Mersenne primes are prime.

See the discussion at the end of [src/number_theory/lucas_lehmer.lean] for ideas about extending this to larger Mersenne primes.

The next four primality tests are too slow to run interactively with -T100000, but work fine on the command line.