I know this is a basic question but I've been struggling to figure this out for the past day and I'm not making progress. I can download and build the source files for mathlib4, and if I just add my own .lean file in that directory then I can import Mathlib without issue, but I can't figure out how to import it from anywhere else. Ideally I would like to add mathlib to the libraries in my toolchain, but I can't find any information on how to do that either. Am I just missing something about how this system is supposed to work?
The ecosystem of lean4 has gone through some changes since lean3, where this was often done via leanproject, so the question isn't necessarily basic. There are multiple ways of doing this (e.g. cloning the whole mathlib4 repo), but the most flexible way is using the new package manager for lean named lake. If you have installed your lean toolchain via elan, you should have a working lake version already. You can then run
lake new <package-name> math
to create a lake package that has mathlib4 as a dependency, check the lakefile.lean in your project, if you want to know more.
Next run
lake build
and you should be good to go!