Formalizing Special Numbers from Concrete Mathematics

Stream: new members

[Walter Moreira]

Hi all, following Knuth's Concrete Mathematics, we have been working on formalizing some facts about the Euclidean numbers in Lean, including the recurrence formula, co-primality and an explicit formula. We have a git repository with the code with the results in the file Euclidean.lean (and also some work in progress code about the Eulerian numbers). For a quick look, this is the auto-generated documentation.

As this is our first real project with Lean, we'd greatly appreciate any feedback. Would some of these topics be a direction that we can follow for contributing to Mathlib?

Many thanks in advance!

Tagging @Joe Stubbs

[Yaël Dillies]

Hey! Good work overall. Here are a few comments:

[Yaël Dillies]

Instead of

theorem euclid_increasing {n : ℕ} : euclid n < euclid (n + 1)

you should prove

theorem euclid_strictMono : StrictMono euclid

using docs#strictMono_nat_of_lt_succ

[Yaël Dillies]

Instead of Nat.gcd a b = 1, you can use docs#Nat.Coprime

[Yaël Dillies]

I have no idea what pl_euc_m stands for. Furthermore, definition names should follow the lowerCamelCase or UpperCamelCase convention

[Yaël Dillies]

All of this is in line for inclusion in mathlib, and would make a great learning opportunity for you. If you are willing to spend some time (more than you think!) getting this into mathlib, please:

1. Request permission to push to non-master branches of the mathlib repo in #mathlib4 > github permission
2. Open a PR from a branch of the mathlib repo (not from a fork)
3. Await comments

[Joe Stubbs]

Thanks! Those are great comments and encouraging feedback. We'll request the permission to push to non-master branches and begin working on addressing the issues you mention above.

[Walter Moreira]

Thank you for the comments!

As a follow-up question: are there guidelines about when to use the private modifier for theorems or definitions that are purely auxiliary? I'm reading over https://leanprover-community.github.io/contribute/style.html to familiarize ourselves, and couldn't find a mention of that feature.

[Yaël Dillies]

I'm not sure about guidelines, but I have personally argued that private is underused and that auxiliary declarations for the purpose of a final result is a perfect use case for it

[Yaël Dillies]

I like how you've used private so far!

[Joe Stubbs]

Hi all, just to follow up on this thread: we created an initial branch and PR with some basic facts about the Euclid numbers. We look for ward to working with the reviewers to get our first contributions into Mathlib!

[Kevin Buzzard]

My personal opinion on these PRs (#20669 and #21244) is that this sequence is a random sequence from OEIS with no particular applications to anything which the community generally agrees is a concrete goal for mathlib (I think "adding all sequences from OEIS to mathlib" is not currently a concrete goal) and thus should be closed as a PR to mathlib. I think this work would be better suited in a different repo, for example an OEIS repo. My worry is that if we add this sequence then it opens a potential floodgate of people adding other OEIS sequences for no reason other than "mathlib has some OEIS sequences".

Of course I would be happy to be overruled here and the comments above only reflect my personal opinion; I'm not speaking for the community or even the maintainers here. I think that an OEIS repo would be quite a cool thing, and one could even imagine linking to it from the OEIS itself. But #20669 came up in the triage meeting as it's been around for a while and perhaps we need to make a decision on it.

[Walter Moreira]

That sounds like a reasonable policy. Thank you for the time the reviewers spent on this. It was a cool experience for us to go over the comments. We’ll look for more useful areas to contribute.