Expansion of mathlib

Stream: new members

[Hanting Zhang]

I've noticed that a lot of projects by students from Xena haven't made it to mathlib. In particular mathlib doesn't have all 3 Sylow's Theorems, even though Chris Hughes has formalized them. Is there a reason for not adding these? Is it a manpower issue, or a refactoring issue, or just "no one has done it yet" (or maybe something else entirely)?

[Mario Carneiro]

Mathlib has some code quality guidelines and a review process, and a lot of people might be good enough to write a proof in lean but aren't bold enough to face the gauntlet of PR process, especially if they've never done it before. This probably requires some kind of mentorship process in order to help guide new users through the experience while maintaining the standards.

[Hanting Zhang]

That makes sense, but how does one get experience if they don't have a direct human mentor? I have a bit of code for nat.fib that I know isn't good enough for mathlib currently. Zulip seems like the obvious place to start, but I haven't seen much "can someone tidy up my code for mathlib?" posts. Presumably because it's tedious and time-consuming, so likely to be ignored? Saying people "aren't bold enough to face the gauntlet of PR process" is not making me feel bold. :/

[Alex J. Best]

We definitely get a "can someone suggest improvements to my code to make it mathlib ready" posts every now and then, less than just general questions about lean, but they do exist. Indeed one of my first posts to this chatroom long ago was a post like this. Personally I would welcome more such posts, and be happy to provide feedback! (nat.fib seems like a great place to start, it is sad that we don't have things like https://proofwiki.org/wiki/Divisibility_of_Fibonacci_Number)
You should also check out https://leanprover-community.github.io/contribute/style.html if you haven't already, and just read through some mathlib files of course, but note that mathlib is not homogenous, some people work a lot in tactic mode, some in term mode only, and some of mathlib was written before we started the current documentation requirements, so it might be best to look at some of the more recently merged PRs on github to get an idea for what the current best practices are.

[Alex J. Best]

Or these two :smile:

import data.nat.fib
import data.nat.gcd
import tactic

open nat
/-- https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime -/
lemma fib_succ_coprime (n : ℕ) : gcd (fib n) (fib $ n + 1) = 1 :=
begin
  induction n with n ih,
  { simp, },
  { convert ih using 1,
    rw [fib_succ_succ, succ_eq_add_one, gcd_rec, add_mod_right, gcd_comm (fib n),
      gcd_rec (fib (n + 1))], },
end
/-- https://proofwiki.org/wiki/Fibonacci_Number_in_terms_of_Smaller_Fibonacci_Numbers -/
lemma fib_add (n m : ℕ) : fib (n + m + 1) = fib (n + 1) * fib (m + 1) + fib n * fib m :=
begin
  induction n with n ih generalizing m ,
  { simp, },
  { rw [(by rw succ_eq_add_one; ac_refl : n.succ + m + 1 = n + (m + 1) + 1), ih,
      fib_succ_succ, fib_succ_succ],
    ring, },
end

[Bryan Gin-ge Chen]

Alex covered a lot of the same ground while I was typing this reply up, but in my opinion, anyone who's read the contributor guidelines (or watched the youtube video linked there) and made an attempt to follow the suggestions there should feel free to request write access to mathlib and submit a PR.

If you're still feeling nervous, you can always read over the open and closed PRs to get a sense of what the review process is like in practice, and you should always feel free to open a new thread here on Zulip for feedback about a potential contribution or if you have any questions about the process.

I haven't seen very many threads here get completely ignored. In my opinion, a thread like "can someone tidy up my code for mathlib" is probably too much to ask for if your code is > 100 lines or so. On the other hand, a similar post phrased like "can I get some suggestions to make this code shorter / faster" would definitely be welcomed (and in my opinion, you'd learn more from working through the suggestions).

[Johan Commelin]

@Hanting Zhang Welcome! If you want to contribute to mathlib, that's great. There are many people here on Zulip that would like to help you.

Back when I started using Lean, my proofs were horrible. I posted something on Zulip, and Patrick Massot said: "Great! Now you should golf your proofs, and clean them up." And I thought: Wait, what? How do I do that. And it took me some time to figure out all the tricks. But many people helped me, and I learned a lot of stuff.

The biggest thing that matters whether someone PRs code to mathlib is

• "you are happy that you finished the proof and want to move on to a new lemma" vs
• "you want to learn how to improve code quality and make the lemmas clean and reusable, and you like the idea of contributing to mathlib"

If you fall in the second category, and you don't mind it if your code goes through 10 iterations of improvements, then you should definitely make a PR. In general this community is very friendly, and we don't mind teaching people all the tricks.
Interaction is key.

[Kevin Buzzard]

I have been very much of the opinion for years now that it's much more important to teach mathematicians to write _any code at all_ than it is to teach them to write mathlib-ready code. I find it a hard enough effort to write mathlib-ready code myself!

[Johan Commelin]

On the other hand, if we want the "library of undergrad maths" to grow (and grow faster), then we should also occasionally teach people to write mathlib-ready code.

[Kevin Buzzard]

People who are interested learn themselves by PRing

[Kevin Buzzard]

Most mathematics that most people write is just stuff like solutions to problem sheet questions and is not at all appropriate for mathlib

[Bryan Gin-ge Chen]

Even if these formalized problem sheet solutions out there aren’t suitable to be added to mathlib, if they rely on mathlib, I think it’d be worthwhile to collect feedback on what parts of the API are missing / hard to use.

[Alistair Tucker]

I have been ignored often enough that now I just maintain a local folder missing_mathlib.

[Kevin Buzzard]

Make PR's!

[Kevin Buzzard]

I was annoyed that the complex numbers were missing in 2017 so I just made a PR, and I didn't have a clue what I was doing at the time!

[Eric Wieser]

Alistair Tucker said:

I have been ignored often enough that now I just maintain a local folder missing_mathlib.

I've started doing this too, but for different reasons - it means you can check your definitions are actually useful to you before immediately PRing them to mathlib. The workflow of

• Add the lemma to missing_mathlib
• Use it in your_project
• Adjust missing_mathlib as your project evolves, which probably makes your lemmas get slightly more general
• Make a PR to upstream bits and pieces of missing_mathlib that you don't expect to change any more
• Repeat

is far more pleasant than

• Add the lemma to mathlib
• Wait 3 hours for it to build
• Go through a few cycles of review
• Upgrade mathlib in your project
• Find the lemma wasn't general enough for your use-cases
• Adjust the lemma in mathlib
• Repeat

[Eric Wieser]

I suspect the level of ignored PRs / messages is higher at the moment due to seasonal holidays though

[Joel Healy]

Call me a conspiracy theorist, but I have this strange feeling that the computer scientists are watching the mathematicians trying to build a mathlib and somewhere in the dark recesses of github they are building a mathematicianlib that will eat it someday! :smile:

[Kevin Buzzard]

I look forward to early retirement and proving the Langlands philosophy at the touch of a button.

[Mario Carneiro]

or disproving...

[Kevin Buzzard]

You clearly have no understanding of how mathematics works

[Mario Carneiro]

lol

[Kevin Buzzard]

It's so beautiful, it must be true.

[Joel Healy]

Ahh. You are a physicist then!

[Kevin Buzzard]

Once I spent a few days learning about Bessel functions, and wrote some code which approximated a certain analytic function on the upper half plane. I evaluated it at two totally random apparently unrelated points and the numbers were equal. It was at this point that I became convinced of everything.

[Kevin Buzzard]

Maybe this is why some physicists like Langlands

[Kevin Buzzard]

The advantage of Langlands is that there is no competing theory. It just works more and more.

[Marc Huisinga]

Kevin Buzzard said:

It was at this point that I became convinced of everything.

everything = Type?

[Kevin Buzzard]

If Langlands is false then it will just be some edge case, people will cheat and redefine what it says. In fact figuring out what it says in full generality is a notoriously tricky problem, and one which I forcefully argued should be fixed as part of my proposal for digitising Langlands (job ad out early Jan!)

[Kevin Buzzard]

Everything is some finset of Props.

[Kevin Buzzard]

But different people have different finsets.

[Joel Healy]

After you knock of Langlands, maybe work on string theory.