Commit 2020-06-06 17:40 589bdb97

feat(number_theory/lucas_lehmer): prime (2^127 - 1) (#2842) This PR

1. proves the sufficiency of the Lucas-Lehmer test for Mersenne primes
2. provides a tactic that uses norm_num to do each step of the calculation of Lucas-Lehmer residues
3. proves 2^127 - 1 = 170141183460469231731687303715884105727 is prime It doesn't
4. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this)
5. use the trick n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1] that is essential to calculating Lucas-Lehmer residues quickly
6. manage to prove any "computer era" primes are prime! (Although my guess is that 2^521 - 1 would run in <1 day with the current implementation.) I think using "the trick" is very plausible, and would be a fun project for someone who wanted to experiment with certified/fast arithmetic in Lean. It likely would make much larger Mersenne primes accessible. This is a tidy-up and completion of work started by a student, Ainsley Pahljina.