Prime Reciprocal Series

Stream: general

[Vladimir Goryachev]

Hello everyone. Me and my friend have formalized the divergence of prime reciprocal series, theorem 81 from the 100 theorems list. However, the code is really messy, as it was almost the first thing we ever did with Lean. What is the best way to make the proof available?

[Vladimir Goryachev]

Also, how are Lean proofs typically licensed, and how should this license be indicated?

[Ruben Van de Velde]

Looks like there's also a PR open: https://github.com/leanprover-community/mathlib/pull/7274

[Johan Commelin]

@Vladimir Goryachev Welcome. Note that #7274 is another PR that deals with nr 81 of the 100 thm list.

Concerning sharing your code: is it 1 file, or multiple files? If it is 1 file, you can post it in a github gist. If it's more files, just post a link to the main file (assuming it's somewhere on github).

[Johan Commelin]

Concerning license, see any file in mathlib https://github.com/leanprover-community/mathlib/blob/master/src/field_theory/abel_ruffini.lean#L1L5

[Vladimir Goryachev]

Thank you. But why then does it say that 81 is not yet formalised in Lean https://leanprover-community.github.io/100-missing.html ?

[Eric Rodriguez]

#7274 is a dead PR as I see it, the author has been MIA for ever

[Eric Rodriguez]

and I don't think they wanted to refactor / add more comments

[Eric Rodriguez]

what proof do you follow Vladimir?

[Vladimir Goryachev]

The proof by Erdos.

[Eric Rodriguez]

same as the other pr then :) that's cool, can you share your code?

[Vladimir Goryachev]

Well, I am not proficient with github yet, but I'll try : )
https://gist.github.com/SymmetryUnbroken/d2bee9459764681b8efbed9b3a6dd16f

[Vladimir Goryachev]

Does it work?

[Johan Commelin]

yes, that works. If you change the extension to .lean then you also get syntax highlighting

[Johan Commelin]

@Vladimir Goryachev are you interested in contributing to mathlib? If so, can you identify a small chunk of code that you think can be reused outside of this proof?

[Johan Commelin]

If you want to contribute to mathlib, a good first step would be to take such a small piece, and PR it to mathlib first.

[Vladimir Goryachev]

Yes, I am interested in contributing to mathlib.

[Vladimir Goryachev]

As for a chunk of code - I have recursively defined the prime-counting function (a function giving the n-th prime number), its inverse (number of primes smaller than a given number), proved that they are inverses, that they are monotone, and that the prime-counting function of n is greater than n. Is this in mathlib yet?

[Bryan Gin-ge Chen]

We've got a page with some tips for contributing to mathlib here: https://leanprover-community.github.io/contribute/index.html

I don't think we have the prime-counting function yet.

[Vladimir Goryachev]

Thank you! I'll try to edit the prime-counting part according to the styleguide and make a PR.

[Vladimir Goryachev]

Actually, I've thought about it, and I don't use any properties of primes there (except that there are infinitely many primes), and I should probably make a general counting function (count (f : N -> Prop) (n : N) : N), which, given a property and an index n, returns the n-th natural number having this property. And then define the inverse of this function, and prove their properties. Is it true that those things aren't implemented yet?

[Yaël Dillies]

I very much suspect that already exists hidden somewhere, with extra carefulness around computability issues. Maybe Mario knows where that is?

[Yaël Dillies]

Another great thing you can do is use encodable. This will allow you to set up an explicit bijection between the naturals and the primes.

[Vladimir Goryachev]

But that would mean using types rather than predicates, right? For example, I would need to use the type of prime numbers, rather than a predicate of being prime.

[Yaël Dillies]

Yes. This type is already defined as nat.primes. I don't know whether switching to types is a good idea, but you can definitely try.

[Vladimir Goryachev]

OK. But this still leaves the question if there is a counting function for predicates - I have briefly browsed the mathlib, and haven't found it yet.

[Johan Commelin]

There is nat.find, but no nat.nth_find. Do you want it to take as arguments (1) the predicate, and (2) a proof that there are infinitely many nats that satisfy the predicate?

[Floris van Doorn]

I looked through the library, and it doesn't seem to exist yet...

[Eric Wieser]

All you need is a proof that there are at least n nats which satisfy the predicate