[Merged by Bors] - feat(number_theory/lucas_lehmer): prime (2^127 - 1) #2842
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
… (units R) < fintype.card R
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
…pow' into lucas_lehmer2
|
I've moved the examples (except for two very trivial and fast ones) to the |
|
This looks good to me now. Are there still comments, or can we merge it? |
bryangingechen
approved these changes
Jun 5, 2020
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
|
Let's get this merged! |
|
I took the liberty of shortening a few proofs. There are quite a few nonterminal On where the tutorials belong: the current setup is fine for now. Ideally, I think someone shouldn't have to read the mathlib source code to figure out how to use a certain interface. If an interface demands explanation beyond doc strings, the tutorials folder seems like the right place. Often these kinds of explanations aren't local to a single file ("how do I use linear algebra?" or "how do I use category theory"?). Spreading tutorial-style examples throughout the library makes it hard to find any of them, hard to generate html, hard to automatically link to them, etc. Certainly we're missing a lot of this kind of documentation right now. The tutorials folder is pretty empty. bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jun 6, 2020
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 1. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this) 2. use the trick `n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]` that is essential to calculating Lucas-Lehmer residues quickly 3. 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.
|
Build failed: |
robertylewis
removed
the
ready-to-merge
|
The build is failing now because of changes to the algebraic hierarchy. |
robertylewis
added
the
awaiting-author
bryangingechen
removed
the
awaiting-author
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jun 6, 2020
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 1. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this) 2. use the trick `n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]` that is essential to calculating Lucas-Lehmer residues quickly 3. 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.
|
Build failed (retrying...): |
bors bot
pushed a commit
that referenced
this pull request
Jun 6, 2020
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 1. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this) 2. use the trick `n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]` that is essential to calculating Lucas-Lehmer residues quickly 3. 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.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
cipher1024
pushed a commit
to cipher1024/mathlib
that referenced
this pull request
Mar 15, 2022
…nity#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 1. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this) 2. use the trick `n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]` that is essential to calculating Lucas-Lehmer residues quickly 3. 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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR
norm_numto do each step of the calculation of Lucas-Lehmer residuesIt doesn't
n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]that is essential to calculating Lucas-Lehmer residues quicklyI 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.