Comment by vitriol83

mathlib and lean are currently too cumbersome for many researchers to use in say algebraic geometry, but maybe more suitable for combinatorics where it has been applied recently.