Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base #17632

Closed
wants to merge 62 commits into from
Closed

[Merged by Bors] - feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base #17632

wants to merge 62 commits into from

Conversation

nielsvoss
Copy link
Collaborator

@nielsvoss nielsvoss commented Nov 19, 2022 •
edited
Loading

A natural number n is a probable prime to base b if n divides b ^ (n - 1) - 1. n is a Fermat pseudoprime to base b if it is a composite probable prime. This commit defines Fermat pseudoprimes and proves that for any positive base b, there exist an infinite number of Fermat pseudoprimes to that base.

An important thing to note about the way I defined Fermat pseudoprimes is that the definition has an edge case where all numbers are Fermat pseudoprimes to base 0 and 1. The case with base 0 is due to the definition involving natural number subtraction. I was told that this definition was not preferable but was otherwise fine, but I can change it if needed.

Since this is my first PR and I am still inexperienced with Lean, a lot of the proofs are very long, but I'm not quite sure about how I would go about shortening them. The lemmas in the helper_lemmas section of this file exist to help prove theorems, but are unrelated to Fermat pseudoprimes.

Some aspects of this PR were discussed in more detail on Zulip.

Open in Gitpod

@nielsvoss nielsvoss added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Dec 2, 2022
@nielsvoss nielsvoss added the awaiting-review The author would like community review of the PR label Dec 4, 2022
@nielsvoss
Copy link
Collaborator Author

I'm not sure how important shortening very long proofs is, but some of the proofs are very long and might be a bit difficult to read. I can probably shorten them, but I would like to make sure that my definitions work before I start doing that.

kbuzzard
kbuzzard reviewed Dec 20, 2022
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've looked at the first 200 or so lines; this is an excellent job for a first PR by the way!

src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
nielsvoss and others added 7 commits December 19, 2022 18:29
@nielsvoss
style(number_theory/fermat_psp): add backticks around variables in do…
b65f783 
…cstrings
@nielsvoss @kbuzzard
style(number_theory/fermat_psp): replace nat.prime n with n.prime
f8895cf 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@nielsvoss
style(number_theory/fermat_psp): golf coprime_of_probable_prime
89001bc 
Use the golfed version of coprime_of_probable_prime provided by Kevin Buzzard.
@nielsvoss @kbuzzard
style(number_theory/fermat_psp): golf probable_prime_iff_modeq
18477fb 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@nielsvoss @kbuzzard
style(number_theory/fermat_psp): use rcases in coprime_of_fermat_psp
eef31aa 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@nielsvoss
style(number_theory/fermat_psp): flip inequality in sub_one_dvd_pow_s…
07defbd 
…ub_one
@nielsvoss
style(number_theory/fermat_psp): replace pow_gt_base with pow_lt_pow
61a512d
kbuzzard
kbuzzard reviewed Dec 20, 2022
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some more comments.

src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
src/number_theory/fermat_psp.lean Outdated Show resolved Hide resolved
nielsvoss and others added 4 commits December 20, 2022 08:44
@nielsvoss @kbuzzard
style(number_theory/fermat_psp): golf pow_gt_exponent
72ed269 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@nielsvoss @kbuzzard
style(number_theory/fermat_psp): use ha.le instead of linarith
3b5f26f 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@nielsvoss @kbuzzard
style(number_theory/fermat_psp): golf pseudoprime_of_base_one
955b231 
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
@nielsvoss
style(number_theory/fermat_psp): golf AB_id_helper
47b1562
@nielsvoss
Copy link
Collaborator Author

Merging the master branch so that mathlib is not outdated in this PR

@nielsvoss
Copy link
Collaborator Author

I moved a large segment of psp_from_prime_psp into a separate lemma, even though this lemma is specific enough that it probably can't be used anywhere else in the file

@nielsvoss
remove unneeded line from proof of psp_from_prime_psp
922a64f
@nielsvoss
simplify use of Fermat's Little Theorem in psp_from_prime_psp
210fd89
@nielsvoss
fix minor error in previous commit
482ff24
@nielsvoss
simplify proof of ha4 in psp_from_prime_psp
19f3a3e
@nielsvoss
simplify proof of ha7 in psp_from_prime_psp
a0198cd
@nielsvoss
simplify proof of ha8 in psp_from_prime_psp
466bd55
@nielsvoss
combine ha7 and ha8 in psp_from_prime_psp
ef33493
@nielsvoss
simplify end of psp_from_prime_psp
a29aa8b
@nielsvoss
fix numbering in exists_infinite_pseudoprimes
f000419
@nielsvoss
remove hi_bpowp_ge_b from psp_from_prime_psp
902b735
@nielsvoss
condense hi_bsquared1 into hi_bsquared in psp_from_prime_psp
23beade
@nielsvoss
add space between infix operators in psp_from_prime_psp
b5d1937
@nielsvoss
simplify proof of hd in psp_from_prime_psp
49e0caf
@nielsvoss
minor edits to module docstring
fffe3e0
@nielsvoss
more minor edits to module docstring
e1e1647
@nielsvoss
add spaces around infix operators and remove unneeded parentheses
031c30f
@nielsvoss
Merge branch 'master' into fermat_psp
51c8036
@nielsvoss
Copy link
Collaborator Author

I did a bit more editing than I expected to psp_from_prime_psp. The overall structure of the proof is the same, but some of the subgoals are shortened slightly. One complex subgoal was factored off into the new private lemma bp_helper.
Aside from that, I tried to add spaces around infix operators wherever possible (though I might have missed a case or two). I also fixed a few errors in the module docstring at the top of the file.

If there are no more changes that I need to make, I will merge this soon.

@riccardobrasca
Copy link
Member

LGTM. Feel free to merge it when CI passes.

@nielsvoss
Copy link
Collaborator Author

Not quite sure why the CI failed. It seemed to get stuck on a completely unrelated file. I think I'm just going to re-run it.

@nielsvoss
Copy link
Collaborator Author

bors r+

1 similar comment
@nielsvoss
Copy link
Collaborator Author

bors r+

@bors
Copy link

bors bot commented Jan 17, 2023

Already running a review

bors bot pushed a commit that referenced this pull request Jan 17, 2023
@nielsvoss
feat(number_theory): prove the existence of infinitely many Fermat ps…
c0439b4 
…eudoprimes to any base (#17632)

A natural number `n` is a probable prime to base `b` if `n` divides `b ^ (n - 1) - 1`. `n` is a Fermat pseudoprime to base `b` if it is a composite probable prime. This commit defines Fermat pseudoprimes and proves that for any positive base `b`, there exist an infinite number of Fermat pseudoprimes to that base.



Co-authored-by: Niels Voss <nvosscode@gmail.com>
@bors
Copy link

bors bot commented Jan 17, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base [Merged by Bors] - feat(number_theory): prove the existence of infinitely many Fermat pseudoprimes to any base Jan 17, 2023
@bors bors bot closed this Jan 17, 2023
@bors bors bot deleted the fermat_psp branch January 17, 2023 02:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@kbuzzard kbuzzard kbuzzard left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@nielsvoss @riccardobrasca @jcommelin @kbuzzard