crowdsourcing mathlib

Stream: general

[Dan]

This has probably been asked before, but I haven't found info on it. Is there opportunity for people to add theorems and lemmas to mathlib as they encounter them in textbooks? Or is the development of mathlib much more formal and team based

[Mario Carneiro]

Please contribute whatever you like, from any source

[Mario Carneiro]

it is not team-based except for a few big projects (which are mostly developing outside mathlib anyway)

[Mario Carneiro]

The majority of contributions are whatever strikes the fancy of individual contributors

[Dan]

awesome, thanks! I'll start looking through the repo and reading about the PR process

[Yaël Dillies]

Most of my contributions are from Bhavik Mehta nerdsniping me with cool bits of maths.

[Stuart Presnell]

The video "Making a pull request to mathlib" (https://www.youtube.com/watch?v=Bnc8w9lxe8A) gives a nice walkthrough of the PR process

[Stuart Presnell]

You can PR something as simple as a single one-liner lemma if you think it would be useful. (Or even less: fixing a typo in some documentation!)

Take a look at some of the recent PRs labelled easy (https://github.com/leanprover-community/mathlib/pulls?q=is%3Apr+label%3Aeasy+) to see some examples.

[Stuart Presnell]

And of course if you have any questions — about whether a particular lemma would be worth PRing, what to name it, which file to put it in, or anything at all — then you're very welcome to ask them here in the Zulip chat.

[Patrick Massot]

I can't get tired of seeing people who started contributing two months ago already being helpful guiding new contributors! Thanks Stuart! :thumbs_up:

[Violeta Hernández]

Most of my contributions are just a way for me to get deep into topics I'm interested in