How to get and Use a copy of Mathlib in lean4?

Stream: lean4

[kvanvels]

I am trying to start a new project that uses a (the?) mathlib library in lean4. I have elan and am using the "nightly" build of lean4.

kvanvel@euler:~/Workspace$ elan --version
elan 1.4.1 (6a7f30d8e 2022-04-15)
kvanvel@euler:~/Workspace$ elan show
installed toolchains
--------------------

stable
leanprover/lean4:nightly (default)
leanprover/lean4:nightly-2022-08-10
leanprover/lean4:stable

active toolchain
----------------

leanprover/lean4:nightly (default)
Lean (version 4.0.0-nightly-2022-08-10, commit e51d892fc2d2, Release)

kvanvel@euler:~/Workspace$ lake new my_project
kvanvel@euler:~/Workspace$ cd my_project/
kvanvel@euler:~/Workspace/my_project$ ls
lakefile.lean  lean-toolchain  Main.lean  MyProject.lean
kvanvel@euler:~/Workspace/my_project$

Is using elan or an equivalent tool the correct way to get a copy of Mathlib? My understanding is there is a port of mathlib from version 3 to version 4, but I can't find documentation of this so I might be misremembering.

Should I clone the "mathlib4" repo and follow the instructions there? If so, should I clone it to a directory in my .elan folder?

I would like to play around with the math stuff, eventually the topology stuff, so I am wondering if it might be better to switch to using lean3.

Any advice and help is appreciated.

[Kevin Buzzard]

If you want to do topology then switch to lean 3 for now. Lean 4 isn't quite ready for mathematics

[Mario Carneiro]

To use mathlib4, you should add it as a dependency in your lakefile like so:

package my_package

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"