Email Gateway (Aug 23 2022 at 08:12): Email Gateway (Aug 23 2022 at 08:12):From: Lawrence Paulson <lp15@cam.ac.uk>
The entries keep coming, and I am happy to welcome Manuel Eberl's "Mersenne primes and the Lucas–Lehmer test".
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.
https://www.isa-afp.org/entries/Mersenne_Primes.html
Larry Paulson
Last updated: Apr 19 2024 at 20:15 UTC