Stream: Is there code for X?
Manuel Candales (Apr 01 2021 at 21:46):
Is the Dirichlet's theorem on arithmetic progressions already implemented, or any of the special cases (like the infinitude of primes of the form 4k+1, 4k-1, etc)?
I didn't find this after doing a google site search or after looking through nat.prime and through the list of 100 theorems.
Kevin Buzzard (Apr 01 2021 at 21:47):
This is a nontrivial theorem; the standard proof involves a bunch of complex analysis and we have essentially no complex analysis. The special cases such as 4k+1, 4k-1 are easily accessible; we have enough about cyclotomic polynomials to do 1 mod N and indeed this might also be done.
Manuel Candales (Apr 01 2021 at 21:49):
I'll like to implement those, if you don't mind. How should I call them (still don't fully get the naming convention), and where should I place them? in nat.prime?
Bhavik Mehta (Apr 01 2021 at 21:51):
https://leanprover-community.github.io/mathlib_docs/number_theory/primes_congruent_one.html Here's the case for 1 mod N
Riccardo Brasca (Apr 01 2021 at 21:51):
As a special case we have docs#nat.exists_prime_ge_modeq_one for primes congruent to
Manuel Candales (Apr 01 2021 at 21:52):
Kevin Buzzard (Apr 01 2021 at 22:23):
If you do 4k-1 you can also do 6k-1, this is the other elementary one. In general you can prove there's infinitely many primes not in a proper subgroup of by elementary methods but you only get a concrete equality when this group has order 2
Bhavik Mehta (Apr 02 2021 at 03:28):
There are a couple more special cases which should be doable without the heavy complex analysis, eg in https://kconrad.math.uconn.edu/blurbs/ugradnumthy/squaresandinfmanyprimes.pdf
Johan Commelin (Apr 02 2021 at 04:38):
Manuel Candales said:
How should I call them (still don't fully get the naming convention)?
Don't worry about that. Once you have a statement in Lean, you can post it here, and then more experienced users will be able to explain to you how to deduce the Lean name from the statement.
Kevin Buzzard (Apr 02 2021 at 08:18):
Yeah if you allow quadratic reciprocity (which we have in mathlib) then you can get a little further. There are very elementary methods (which don't use Z/pZ^* cyclic) for classifying when -1 and -3 are squares mod p which is why you don't even need QR for the cases I originally mentioned
Mario Carneiro (Apr 02 2021 at 08:23):
I would be remiss to not mention the proof of dirichlet's theorem in the form "every arithmetic progression contains infintely many primes" done in lean by translation from metamath. See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20number.20theorem.20in.20lean/near/168472336
Mario Carneiro (Apr 02 2021 at 08:25):
It's not in mathlib, though, because it has a dependency on the metamath library
Last updated: May 17 2021 at 15:13 UTC