Comment by mejutoco

I dont think mathlib is mandatory to use lean.