Lean is too inflexible for this, in my opinion. Maybe I'm not dreaming big enough, but I think there'll have to be one more big idea to make this possible; I think the typeclass inference systems we use these days are a severe bottleneck, for one, and I think it's very, very tedious to state some things in Lean (my go-to example is the finite-dimensionality of modular forms of level 1 - the contour integral is a bitch and has a lot of technicalities)