Mathlib is one of the world’s largest libraries of mathematics, written in a single language (Lean).
The aim of this blog is certainly not to teach Lean or even to be a reference for Mathlib. I simply want to make pure mathematics more approachable by describing the fields that exist and when they can be used. I do try to link to more comprehensive references so that readers that are interseted in a topic can easily dive in to properly learn more. Mathlib is a sort of universal reference in this sense - it is the largest single source that can be consulted for any field of math, and it is verified by both humans and machines to be correct.
I would be remiss not to link to such a vast body of knowledge, and slowly teach dedicated readers to traverse it on their own.