is mathlib made only by the community?

Stream: mathlib4

[crab]

is mathlib made only by the community or is it mainly supported by the official lean staff. the whole documentation and information is on the leanprover community website

[Henrik Böving]

mathlib is being mainly maintained by the lean community including both computer scientists and mathematicians that are students, professors, postdocs etc.

mathlib4 (which I assume you are asking about since you are in the mathlib4 stream) is a project that is doing experiments for when the original mathlib eventually gets ported from Lean 3 to Lean 4, it's not an official Lean project either but Gabriel (who is at least part of the official Lean org on Github, dunno whether that is considered "official Lean staff") has written large amounts of code in it.

[Mario Carneiro]

There isn't really any such thing as "official lean staff", although there are a few paid positions with enough freedom to permit working on lean nearly full time

[Mario Carneiro]

Furthermore, mathlib has always been somewhat separate from lean core development, and it has always been a volunteer project. (Things are starting to change lately, there is more support from MS now than there has been in the past, but it's still fairly independent and there is no one on the MS payroll who works on mathlib full time AFAIK.)

[crab]

I see. this makes sense. I hope to contribute to mathlib one day