contributing to mathlib

Stream: mathlib4

[İmran Tanrikolu]

**What are the academic, professional, and personal benefits of contributing to mathlib?
How can I contribute to mathlib?
Is contributing really important?
Where can I find topics that are missing from mathlib?**

[Michael Rothgang]

Hi! Contributions to mathlib are very welcome, there's lots of work to be done --- so glad to hear you're interested.

[Michael Rothgang]

I'm not sure what you're asking, though: your questions seem very generic --- what do you really want to know?

[Michael Rothgang]

If you tell us more about your background/what you know and are interested in, we can suggest suitable topics. As-is, mathlib is broad enough that trying to mention every possible project is not feasible.

[Michael Rothgang]

Besides, the answers to your question depend on your situation. For example,

• contribution to mathlib is obviously important for mathlib; I believe we really need a common ground of shared definitions and results if we want e.g. formalisation of research papers to become more standard
• contributing to mathlib got me my current job, which makes me much happier than my previous one -- so this can be very useful. But this will vary from person to person.

[Michael Rothgang]

In other words: if you tell us what you actually want to know, there's a chance we can answer your actual questions.

[Weiyi Wang]

not necessarily the optimal way, but I find https://leanprover-community.github.io/1000-missing.html a good starting point to find missing topics in mathlib. (someone might be already working on some though, so also search open PR and zulip discussion)

[Ruben Van de Velde]

So if you contribute to mathlib, you too can have @Michael Rothgang's job! (Wait, maybe that's not the goal here)