| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Mersenne primes and the Lucas–Lehmer test
| Title: | Mersenne primes and the Lucas–Lehmer test |
| Author: | Manuel Eberl |
| Submission date: | 2020-01-17 |
| Abstract: |
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. |
| BibTeX: |
@article{Mersenne_Primes-AFP,
author = {Manuel Eberl},
title = {Mersenne primes and the Lucas–Lehmer test},
journal = {Archive of Formal Proofs},
month = jan,
year = 2020,
note = {\url{https://isa-afp.org/entries/Mersenne_Primes.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Native_Word, Pell, Probabilistic_Prime_Tests |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |