State of mathlib4?

Stream: mathlib4

[Lyle Kopnicky]

Hi folks, I was using Lean 3 a few years ago and doing some simple arithmetic and logic proofs. Never used mathlib. Now I want to do some simple proofs in topology and category theory. I saw that Lean 4 was available, so I thought it's better to switch to that and learn it. I've gotten it installed. What's the state of mathlib4? How would I install it? Can I do some simple topology? Thanks!

[Patrick Massot]

This is too early. mathlib4 is not ready for use.

[Lyle Kopnicky]

OK, thank you. I'll stick with Lean 3 for now.

[Henrik Böving]

It is over here https://github.com/leanprover-community/mathlib4 but its far far away from those advanced topics and also not meant to be the final product, some time in the future :tm: we will automatically port large parts of mathlib 3 to 4 and that will be the actual mathlib4, the current repo is just for experimentation mostly.