Sum of prime reciprocals diverges

Stream: new members

[Nick Pilotti]

I was surprised to see the proof of the divergence of the prime reciprocal series on the list of theorems not proven yet in Lean. It seems all this would require is the Euler product formula (which requires unique factorization and basic properties of convergence), the power series expansion of log and that the harmonic series diverges. Is there any reason this hasn't been proved yet in Lean?

[Johan Commelin]

I think I saw someone else working on it a month ago or so. I'll try to find it.

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Prime.20Reciprocal.20Series

[Johan Commelin]

Also: https://github.com/leanprover-community/mathlib/pull/7274/files

[Johan Commelin]

@Nick Pilotti By the way, Welcome! :wink:

[Nick Pilotti]

Thanks, I'll have a look

[Nick Pilotti]

On a related note, has there ever been any work towards proving Dirichlet's theorem? It would require a decent amount of complex analysis and some group theory to make defining characters easier. Some of the identities needed seem like they might be tricky to prove.

[Kevin Buzzard]

Let me stop you at the complex analysis bit

[Kevin Buzzard]

We have to be patient here, we don't have complex analysis yet but it's coming and my understanding is that people do understand how it's going to be done. Yes it's holding up a lot of things, but that's just a proof of how mathematics is strongly interconnected beyond some point.

[Nick Pilotti]

I figured it might be something like that. I'm still figuring out what mathlib can and can't do. Thanks

[Kevin Buzzard]

I remember someone pointing out a couple of years ago that lean could do perfectoid spaces but not graphs (although this is no longer true). This is a good example demonstrating that these things are not always easy to guess...

[Yaël Dillies]

We can still can't do much graph... :sad: But Kyle's branch will change that once it gets into mathlib.

[Will Sawin]

Yaël Dillies said:

We can still can't do much graph... :sad: But Kyle's branch will change that once it gets into mathlib.

I had to check that there is an example of a graph other than the empty graph .... :smile:

[Kevin Buzzard]

There are infinitely many examples of perfectoid spaces in the perfectoid repo -- an empty one for each prime number

[Scott Morrison]

On the other hand, we still run out of primes at 2^127 - 1, since no one has taken the low hanging-fruit of making src#lucas_lehmer run fast yet. :-)

[Vladimir Goryachev]

@Nick Pilotti Yes, we are working on divergence of reciprocal primes, following the proof by Erdos. At the moment, we have defined the "nth prime" function (actually, nth element of any set of natural numbers), and proved some theorems about the function. We plan to add it to mathlib soon. Then the next step, I guess, would be unique separation of a natural number into a product of a square and a squarefree number.

[Eric Rodriguez]

speaking of that, Vlad, do you want to PR it? :) I think it's ready

[Vladimir Goryachev]

Well, my computer got broken, so I could not get to Lean for about a weak. I hope to get it back today, and PR the count file if it is not done yet.

[Yaël Dillies]

Oh sorry to hear that. We left you the pleasure to open the PR :smile:

[Yaël Dillies]

You did most of the heavy lifting.

[Vladimir Goryachev]

Thanks! :-)

[Yaël Dillies]

@Michael Stoll, I just noticed you proved docs#not_summable_one_div_on_primes, but we also have docs#Theorems100.Real.tendsto_sum_one_div_prime_atTop. Were you aware?

[Yaël Dillies]

Or, rather, you seem to be aware, but do you have plans to unify both files?

[Michael Stoll]

I was not aware of it when I did the proof, but I noticed when updating the list. I was wondering why it was not in Mathlib in the first place...

[Yaël Dillies]

I didn't check, are both proofs following the same argument or is your more high-powered somehow?

[Michael Stoll]

What would a unification look like? Include the spelling of docs#Theorems100.Real.tendsto_sum_one_div_prime_atTop in Mathlib.NumberTheory.SumPrimeReciprocals?

[Yaël Dillies]

Yes, and maybe delete the file in the archive assuming your proof is similar enough

[Michael Stoll]

OK; I may do this eventually, but it is not high priority.