Zulip Chat Archive

Stream: new members

Topic: Expansion of mathlib


view this post on Zulip Hanting Zhang (Dec 31 2020 at 00:02):

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)?

view this post on Zulip Mario Carneiro (Dec 31 2020 at 00:08):

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.

view this post on Zulip Hanting Zhang (Dec 31 2020 at 00:22):

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. :/

view this post on Zulip Alex J. Best (Dec 31 2020 at 00:43):

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.

view this post on Zulip Alex J. Best (Dec 31 2020 at 00:45):

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

view this post on Zulip Bryan Gin-ge Chen (Dec 31 2020 at 00:48):

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).

view this post on Zulip Johan Commelin (Dec 31 2020 at 05:37):

@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.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 07:24):

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!

view this post on Zulip Johan Commelin (Dec 31 2020 at 07:42):

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.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 07:45):

People who are interested learn themselves by PRing

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 07:47):

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

view this post on Zulip Bryan Gin-ge Chen (Dec 31 2020 at 08:16):

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.

view this post on Zulip Alistair Tucker (Dec 31 2020 at 12:03):

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

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 12:04):

Make PR's!

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 12:05):

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!

view this post on Zulip Eric Wieser (Dec 31 2020 at 12:15):

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

view this post on Zulip Eric Wieser (Dec 31 2020 at 12:16):

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

view this post on Zulip Joel Healy (Dec 31 2020 at 17:42):

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:

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:43):

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

view this post on Zulip Mario Carneiro (Dec 31 2020 at 17:44):

or disproving...

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:44):

You clearly have no understanding of how mathematics works

view this post on Zulip Mario Carneiro (Dec 31 2020 at 17:44):

lol

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:45):

It's so beautiful, it must be true.

view this post on Zulip Joel Healy (Dec 31 2020 at 17:45):

Ahh. You are a physicist then!

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:46):

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.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:46):

Maybe this is why some physicists like Langlands

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:47):

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

view this post on Zulip Marc Huisinga (Dec 31 2020 at 17:48):

Kevin Buzzard said:

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

everything = Type?

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:48):

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!)

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:48):

Everything is some finset of Props.

view this post on Zulip Kevin Buzzard (Dec 31 2020 at 17:49):

But different people have different finsets.

view this post on Zulip Joel Healy (Dec 31 2020 at 17:50):

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


Last updated: May 11 2021 at 00:31 UTC