Mathlib is an online, evolving, collaborative project, aiming to be a foundation for all of modern pure mathematics. It is fully searchable, and here is its homepage. It is hosted on github, and it is all checked with the Lean Theorem Prover.
A great place to see the current state of mathlib is this overview page, which the community keeps up to date.
There are still some parts of undergraduate mathematics not covered by mathlib, but on the other hand there is plenty of advanced mathematics there; for example recent (2020) achievements include a bunch of MSc level commutative algebra (e.g. DVRs), a start on homological algebra, Lie algebras, a bunch of abstract measure theory and Haar measure, manifolds and bundles. My list will go out of date quickly however -- check out the overview page for recent achievements.
Around 100 people have contributed so far, ranging from high school kids to full professors;professors (in particular it is genuinely collaborative); all you have to do is to learn the Lean programming language so you can express mathematics in Lean, and then formalise something that we want in the library. We welcome contributions from many areas of mathematics -- as well as standard UG and MSc material in number theory, geometry, topology, analysis and algebra there is combinatorial game theory, Euclidean geometry and lots of other things. Here is a list of undergraduate-level material which we still do not have.
Three years ago the library had essentially nothing (no complex numbers, no sine and cosine, for example). But it is growing fast and my personal belief is that ultimately it is a more modern way of presenting mathematics than the Stacks Project and Kerodon. Within the next few years, all being well, part of mathlib will be integrating with the Stacks Project; both the mathlib people and the stacks project people are interested in the collaboration, and this recent PR by Scott Morrison (one of the founders of MathOverflow!) is another stepping stone towards schemes; we should have them in mathlib within the next few weeks (they already exist in Lean code but we have learnt the hard way that stuff not in mathlib is liable to bitrot). The reason I think mathlib will ultimately be more important that the Stacks Project or Kerodon is that mathlib is machine-readable, enabling computers to read research-level mathematics. Unfortunately computers still cannot understand natural language, meaning that it is difficult for AI to use e.g. ArXiv to do mathematics at research level, so right now it seems to me that formalisation is a natural way to proceed. I believe that it is inevitable that one day machines will be doing mathematics well, just like it was inevitable that one day they would play chess and go well; indeed one of the reasons I am motivated to work on mathlib is that I want machines to do arithmetic geometry well and this will only happen if professional arithmetic geometers like me explain arithmetic geometry to a computer.
People interested in contributing can take a look at the Zulip chat -- this is a focussed chat room where people use their real names and experts work on questions which have arisen from the formalisation of mathematics. There are sometimes 1000 posts in a day and a lot of the conversation is highly technical, but there is a #new members stream where beginners can ask questions. Please read the community guidelines. In short -- be nice. It's as simple as that.
Mathematicians wishing to learn something about how to contribute might find the Youtube videos from last month's introductory workshop Lean for the curious mathematician interesting. There is also the ongoing book Mathematics in Lean.